leanprover-community/mathlib3

Pull Requests Commits

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

refactor(group_theory/commutator): Use commutator notation in `commutator_normal` (#12575)

tb65536 committed 3 years ago

6c04fcf4

feat(algebra/group/to_additive + a few more files): make `to_additive` convert `unit` to `add_unit` (#12564)

adomani committed 3 years ago

84cbbc98

feat(data/zmod/basic): some lemmas about coercions (#12571)

eric-wieser committed 3 years ago

869ef84f

chore(*): clear up some excessive by statements (#12570)

alexjbest committed 3 years ago

6fdb1d5d

feat(field_theory/is_alg_closed/basic): add `is_alg_closed.infinite` (#12566)

Jlh18 committed 3 years ago

45c22c0d

feat(tactic/norm_num_command): add user command to run norm_num on an expression (#12550)

kmill committed 3 years ago

0e93816c

Older