leanprover-community/mathlib3

Pull Requests Commits

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

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

leanprover-community-bot committed 4 years ago

128c0965

feat(*/sort): sorting empty sets/singletons (#12801)

ericrbg committed 4 years ago

7764c604

feat(topology/{order,separation}): several lemmas from an old branch (#12794)

urkud committed 4 years ago

d04fff95

feat(algebra/char_p/two): add `simp` attribute to some lemmas involving characteristic two identities (#12800)

adomani committed 4 years ago

7f1ba1a3

feat(linear_algebra/sesquilinear_form): preliminary results for nondegeneracy (#12269)

mcdoll committed 4 years ago

e282089f

feat(group_theory/nilpotent): the is_nilpotent_of_finite_tfae theorem (#11835)

nomeata committed 4 years ago

076490ae

feat(ring_theory/unique_factorization_domain): some lemmas relating shapes of factorisations (#9345)

Paul-Lez committed 4 years ago

8c89ae6f

doc(src/tactic/doc_commands): typo “between” → “better” (#12804)

nomeata committed 4 years ago

0c52d3b4

Newer Older