leanprover-community/mathlib3

Pull Requests Commits

Update src/field_theory/adjoin.lean

Sebastian-Monnet committed 3 years ago

Verified 6216f91e

Update src/field_theory/krull_topology.lean

Sebastian-Monnet committed 3 years ago

Verified c4892c4f

Update src/field_theory/krull_topology.lean

Sebastian-Monnet committed 3 years ago

Verified dbb4b469

fixed indentation

Sebastian-Monnet committed 3 years ago

e7c275b0

changed definition of ultrafilter.glued_generators_of_pushforwards_function to term style

Sebastian-Monnet committed 3 years ago

c92b376b

changed from intermediate_field to is_scalar_tower

Sebastian-Monnet committed 3 years ago

a59c802d

Merge branch 'alg_hom_of_ultrafilter' of https://github.com/leanprover-community/mathlib into alg_hom_of_ultrafilter

Sebastian-Monnet committed 3 years ago

35676b88

changed to nhds syntax

Sebastian-Monnet committed 3 years ago

802cd58c

put arguments on one line

Sebastian-Monnet committed 3 years ago

99ffb64e

Update src/field_theory/krull_topology.lean

Sebastian-Monnet committed 3 years ago

Verified 969f0ef6

remove unused lemma from another PR

eric-wieser committed 3 years ago

4307e385

fix a previous bad merge

eric-wieser committed 3 years ago

609fc302

Merge remote-tracking branch 'origin/master' into alg_hom_of_ultrafilter

eric-wieser committed 3 years ago

804c4660

feat(ring_theory): Basic framework for classes of ring homomorphisms (#14966)

erdOne committed 3 years ago

073c3ace

chore(scripts): update nolints.txt (#15332)

leanprover-community-bot committed 3 years ago

e479bfbe

chore(set_theory/pgame): remove redundant `dsimp` (#15312)

vihdzp committed 3 years ago

b89df0ab

chore(data/matrix/block): lemmas about swapping blocks of matrices (#15298)

eric-wieser committed 3 years ago

4302cb7e

doc(set_theory/ordinal/cantor_normal_form): document most theorems (#15227)

vihdzp committed 3 years ago

5590b0a2

chore(order/order_iso_nat): remove `decidable_pred` assumption from `subtype.order_iso_of_nat` (#15190)

vihdzp committed 3 years ago

5744b50d

feat(data/finset/basic): Add `decidable_nonempty` for finsets. (#15170)

linesthatinterlace committed 3 years ago

08648056

feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542)

Michael14071407 committed 3 years ago

1e82f5ec

feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311)

fpvandoorn committed 3 years ago

f7313156

feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309)

fpvandoorn committed 3 years ago

25f60b46

feat(tactic/linear_combination): add parser for `h / a` (#15284)

digama0 committed 3 years ago

51f76d05

feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields (#15022)

ericrbg committed 3 years ago

be53c7cb

feat(combinatorics/additive/behrend): Behrend's construction (#14070)

YaelDillies committed 3 years ago

44999a92

feat(set_theory/ordinal/basic): mark `type_fintype` as `simp` (#15194)

vihdzp committed 3 years ago

2084baf2

refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` (#15191)

eric-wieser committed 3 years ago

93e164e8

Update ultrafilter.lean

eric-wieser committed 3 years ago

Verified 9cfe121f

Merge branch 'master' into alg_hom_of_ultrafilter

eric-wieser committed 3 years ago

Verified a9e43730

Older