Commits leanprover-community/mathlib

chore(set_theory/ordinal_arithmetic): golf proof into term mode (#11691)

vihdzp committed 3 years ago

74584760

doc(polynomial/eval): why map_ring_hom can't replace map (#11537)

ericrbg committed 3 years ago

02c08d9b

feat(archive/100-theorems-list): add proof of the solution of the cubic (#11635)

null-lambda committed 3 years ago

05e1845c

feat(set_theory/ordinal_arithmetic): Update header (#11681)

vihdzp committed 3 years ago

08445971

feat(set_theory/ordinal_arithmetic): Proved `sup_eq_lsub_iff_lt_sup` (#11660)

vihdzp committed 3 years ago

a6ace8c1

chore(analysis/complex/cauchy_integral): use `dslope` to golf a proof (#11675)

urkud committed 3 years ago

92ee748e

feat(order/filter): +1 version of `mem_inf_principal` (#11674)

urkud committed 3 years ago

a1e1ffd1

chore(*): don't use tactic internal lemmas in proofs (#11641)

alexjbest committed 3 years ago

52e9fd52

chore(topology/algebra/uniform_group): Remove newline after docstring (#11671)

tb65536 committed 3 years ago

577e3a22

feat(data/nat/factorization): various theorems on factorization and division (#11663)

stuart-presnell committed 3 years ago

946454a8

feat(group_theory/free_abelian_group_finsupp): various equiv.of_free_*_group lemmas (#11469)

nomeata committed 3 years ago

97e01cda

feat(data/{dfinsupp,finsupp}/basic): `fun_like` instances for `Π₀ i, α i` and `ι →₀ α` (#11667)

YaelDillies committed 3 years ago

8fbc009a

feat(algebraic_geometry): Stalk is localization of affine open. (#11640)

erdOne committed 3 years ago

c447a31c

feat(data/nat/basic): three small `dvd_iff...` lemmas (#11669)

stuart-presnell committed 3 years ago

b8fcac51

refactor(topology/algebra/uniform_group): Use `to_additive`. (#11662)

tb65536 committed 3 years ago

c5a8a818

feat(group_theory/subgroup/basic): add lemmas related to map, comap, normalizer (#11637)

nomeata committed 3 years ago

5472f0a7

feat(group_theory/sylow): add characteristic_of_normal (#11636)

nomeata committed 3 years ago

2b257230

feat(analysis/inner_product_space/basic): isometries and orthonormal families (#11631)

jsm28 committed 3 years ago

1a72f887

feat(measure_theory/measure/haar_lebesgue): a density point for closed balls is a density point for rescalings of arbitrary sets (#11620)

sgouezel committed 3 years ago

631f3394

feat(analysis/seminorm): The norm as a seminorm, balanced and absorbent lemmas (#11487)

YaelDillies committed 3 years ago

590b5eb4

feat(analysis/seminorm): add some lemmas for seminorm balls (#11471)

mcdoll committed 3 years ago

573ca836

feat(combinatorics/configuration): Formula for cardinality of a projective plane (#11462)

tb65536 committed 3 years ago

07d8ca6d

feat(algebra/order/hom/monoid): Ordered monoid/group homomorphisms (#11633)

YaelDillies committed 3 years ago

7f0f3f19

feat(order/hom/lattice): Lattice homomorphisms (#11610)

YaelDillies committed 3 years ago

20aae835

feat(group_theory/subgroup/basic): add normalizer_condition definition (#11587)

nomeata committed 3 years ago

09c6ce81

feat(topology/*): replace some `a < b` assumptions with `a ≠ b` (#11650)

urkud committed 3 years ago

c294e4bb

feat(algebra/big_operators/order): The size of a finset of disjoint finsets is less than the size of its union (#11654)

YaelDillies committed 3 years ago

20a461f3

refactor(set_theory/ordinal_arithmetic): Rename `lsub_le_iff_lt` to `lsub_le` (#11661)

vihdzp committed 3 years ago

b237af52

chore(data/buffer/parser/numeral): fix backticks (#11658)

ericrbg committed 3 years ago

b0a18124

feat(analysis/special_functions/complex/circle): `real.angle.exp_map_circle` (#11627)

jsm28 committed 3 years ago

033dd3c5