leanprover-community/mathlib

Pull Requests Commits

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

Ruben-VandeVelde committed 3 years ago

42dcf354

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

tb65536 committed 3 years ago

3ba1c023

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

Multramate committed 3 years ago

52b9b36b

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

urkud committed 3 years ago

245b614e

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

adomani committed 3 years ago

dae6155d

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

eric-wieser committed 3 years ago

1d183094

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

tb65536 committed 3 years ago

ef69547c

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

eric-wieser committed 3 years ago

ee4472b6

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

YaelDillies committed 3 years ago

c9fc9bf7

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

riccardobrasca committed 3 years ago

2b6b9ffc

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

gebner committed 3 years ago

4c60258c

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

leanprover-community-bot committed 3 years ago

128c0965

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

ericrbg committed 3 years ago

7764c604

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

urkud committed 3 years ago

d04fff95

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

adomani committed 3 years ago

7f1ba1a3

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

mcdoll committed 3 years ago

e282089f

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

nomeata committed 3 years ago

076490ae

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

Paul-Lez committed 3 years ago

8c89ae6f

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

nomeata committed 3 years ago

0c52d3b4

doc(archive/100-theorems-list/9_area_of_a_circle): fix `×` (#12803)

ericrbg committed 3 years ago

d3703fe9

chore(model_theory/definability): Change variable order in definability (#12802)

awainverse committed 3 years ago

f4e7f82a

feat(order/rel_iso): Add `subrel` instances (#12758)

vihdzp committed 3 years ago

f6e85fc4

feat(set_theory/*): Redefine `sup f` as `supr f` (#12657)

vihdzp committed 3 years ago

fdd7e98c

feat(model_theory/terms_and_formulas): Atomic, Quantifier-Free, and Prenex Formulas (#12557)

awainverse committed 3 years ago

290ad757

feat(category_theory/abelian) : injective resolutions of an object in a category with enough injectives (#12545)

jjaassoonn committed 3 years ago

d17ecf9e

feat(model_theory/terms_and_formulas): Language maps act on terms, formulas, sentences, and theories (#12609)

awainverse committed 3 years ago

80b8d191

feat(archive/100-theorems-list): add proof of thm 81 (#7274)

manuelcandales committed 3 years ago

bf690dd3

feat(data/nat/prime): add two lemmas with nat.primes, mul and dvd (#12780)

adomani committed 3 years ago

b49bc778

fix(ring_theory/power_series/basic): remove duplicate instance (#12744)

kbuzzard committed 3 years ago

5a547aa9

feat(number_theory/arithmetic_function): add eq of multiplicative functions (#12689)

khwilson committed 3 years ago

14ee5e03

Older