leanprover-community/mathlib3

Pull Requests Commits

refactor(group_theory/commutator): Move and golf `commutator_le` (#12599)

tb65536 committed 3 years ago

2e7483d2

chore({category_theory,order}/category/*): Missing `dsimp` lemmas (#12593)

YaelDillies committed 3 years ago

09d0f028

feat(data/nat): add card_multiples (#12592)

Ruben-VandeVelde committed 3 years ago

4e302f54

feat(algebra/group/units_hom): make `is_unit.map` work on `monoid_hom_class` (#12577)

eric-wieser committed 3 years ago

222faeda

feat(category_theory): interderivability of kernel and equalizers in preadditive cats (#12576)

javra committed 3 years ago

8364980d

chore(*): update to 3.41.0c (#12591)

kmill committed 3 years ago

c0a51cf2

feat(algebra/module): add `module.nontrivial` (#12594)

urkud committed 3 years ago

e7db1936

feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib (#12524)

nomeata committed 3 years ago

5856c0c4

feat(set_theory/ordinal_arithmetic): Further theorems on normal functions (#12484)

vihdzp committed 3 years ago

dc5f7fbf

feat(data/list/prod_monoid): add prod_eq_pow_card (#12473)

nomeata committed 3 years ago

e3ad468b

feat(order/monotone): Folds of monotone functions are monotone (#12581)

vihdzp committed 3 years ago

7dcba96e

feat(linear_algebra/projective_space/basic): The projectivization of a vector space. (#12438)

adamtopaz committed 3 years ago

3dcc1689

feat(model_theory/substructures): Facts about substructures (#12258)

awainverse committed 3 years ago

003701f0

feat(set_theory/ordinal_arithmetic): The derivative of multiplication (#12202)

vihdzp committed 3 years ago

d6f337df

feat(algebra/order/monoid): add `with_zero.canonically_linear_ordered_add_monoid` (#12568)

eric-wieser committed 3 years ago

e6fef397

feat(order/sup_indep): add `finset.sup_indep_pair` (#12549)

eric-wieser committed 3 years ago

12786d04

chore(topology/algebra/module/basic): cleanup variables and coercions (#12542)

eric-wieser committed 3 years ago

4dc4dc8b

refactor(group_theory/commutator): Golf some proofs (#12586)

tb65536 committed 3 years ago

02e0ab2c

feat(order/hom): `prod.swap` as an `order_iso` (#12585)

urkud committed 3 years ago

d9a774e2

feat(data/list/basic): Miscellaneous `fold` lemmas (#12579)

vihdzp committed 3 years ago

840a0425

refactor(group_theory/solvable): Golf proof (#12552)

tb65536 committed 3 years ago

1a581ede

feat(analysis/special_functions): limit of x^s * exp(-x) for s real (#12540)

loefflerd committed 3 years ago

1326aa7c

refactor(algebra/group/to_additive): monadic code cosmetics (#12527)

nomeata committed 3 years ago

e553f8ad

feat(data/setoid/partition): Relate `setoid.is_partition` and `finpartition` (#12459)

AntoineChambert-Loir committed 3 years ago

47b1ddf2

fix(probability): remove unused argument from `cond_cond_eq_cond_inter` (#12583)

rish987 committed 3 years ago

115f8c7a

feat(data/nat/{nth,prime}): add facts about primes (#12560)

kmill committed 3 years ago

3061d18f

feat(group_theory/commutator): Add some basic lemmas (#12554)

tb65536 committed 3 years ago

de4d14cb

refactor(group_theory/commutator): Golf proof of `commutator_mem_commutator` (#12584)

tb65536 committed 3 years ago

355472dc

feat(data/list/basic): Lists over empty type are `unique` (#12582)

vihdzp committed 3 years ago

b5a26d0a

refactor(group_theory/commutator): Use commutators in `commutator_le` (#12572)

tb65536 committed 3 years ago

f0dd6e9b

Older