leanprover-community/mathlib3

Pull Requests Commits

feat(model_theory/ultraproducts): Ultraproducts and the Compactness Theorem (#12531)

awainverse committed 4 years ago

8161ba28

feat(measure_theory/constructions/borel_space): generalize a lemma (#12843)

urkud committed 4 years ago

8e9abe3c

chore(category/abelian/derived): shorten proof (#12847)

jjaassoonn committed 4 years ago

d902c222

feat(algebra/homology/additive): dualise statement of chain complex to cochain complex (#12840)

jjaassoonn committed 4 years ago

395019ee

feat(polynomial/derivative): tidy+new theorems (#12833)

ericrbg committed 4 years ago

69d3d16b

feat(order/compare): add 4 dot notation lemmas (#12832)

urkud committed 4 years ago

06017e07

chore(data/real/basic): tweak lemmas about `of_cauchy` (#12829)

eric-wieser committed 4 years ago

f5987b2a

feat(ring_theory/algebraic): Added basic lemmas + golf (#12820)

vihdzp committed 4 years ago

772c7766

feat(data/rat/denumerable): Make `mk_rat` into a simp lemma (#12821)

vihdzp committed 4 years ago

60af3bda

feat(analysis/locally_convex): define von Neumann boundedness (#12449)

mcdoll committed 4 years ago

656f7494

refactor(group_theory/group_action/basic): Golf definition of action on cosets (#12823)

tb65536 committed 4 years ago

9502db1f

feat(category_theory/abelian/*): add some missing lemmas (#12839)

jjaassoonn committed 4 years ago

f2fa1cf9

chore(ring_theory/algebraic): fix typo + golf (#12834)

vihdzp committed 4 years ago

cdd05728

feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem (#12787)

j-loreaux committed 4 years ago

6abfb1d7

chore(ring_theory/ideal): use `ideal.mul_mem_left` instead of `submodule.smul_mem` (#12830)

eric-wieser committed 4 years ago

cd012fbe

feat(category_theory): (co)equalizers and (co)kernels when composing with monos/epis (#12828)

javra committed 4 years ago

f1200764

refactor(analysis/seminorm): move topology induced by seminorms to its own file (#12826)

mcdoll committed 4 years ago

49cd1cc6

feat(group_theory/group_action/basic): Right action of normalizer on left cosets (#12822)

tb65536 committed 4 years ago

2660d16d

chore(*): update to lean 3.42.0c (#12818)

kmill committed 4 years ago

48eacc63

chore(algebra/char_p/exp_char): golf char_eq_exp_char_iff (#12825)

Ruben-VandeVelde committed 4 years ago

42dcf354

feat(group_theory/subgroup/basic): Alternate version of `mem_normalizer_iff` (#12814)

tb65536 committed 4 years ago

3ba1c023

feat(ring_theory/fractional_ideal): fractional ideal is one if and only if ideal is one (#12813)

Multramate committed 4 years ago

52b9b36b

chore(measure_theory/measure): move subtraction to a new file (#12809)

urkud committed 4 years ago

245b614e

chore(number_theory/primorial): golf a proof (#12807)

adomani committed 4 years ago

dae6155d

feat(linear_algebra/determinant): no need for `is_domain` (#12805)

eric-wieser committed 4 years ago

1d183094

feat(group_theory/finiteness): Define the minimum number of generators (#12765)

tb65536 committed 4 years ago

ef69547c

feat(group_theory/group_action/embedding): group actions apply on the codomain of embeddings (#12798)

eric-wieser committed 4 years ago

ee4472b6

refactor(order/filter/pointwise): Cleanup (#12789)

YaelDillies committed 4 years ago

c9fc9bf7

feat(category_theory/abelian/derived): add left_derived_zero_iso_self (#12403)

riccardobrasca committed 4 years ago

2b6b9ffc

chore(ring_theory/dedekind_domain/ideal): golf (#12737)

gebner committed 4 years ago

4c60258c

Newer Older