leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/algebra/basic): add `algebra.coe_linear_map`

eric-wieser committed 4 years ago

Verified a538cf42

chore(measure_theory/measure): review API of `mutually_singular` (#10186)

urkud committed 4 years ago

ae98aad6

refactor(measure_theory/function/l1_space): remove hypothesis (#10185)

fpvandoorn committed 4 years ago

7a8a9146

chore(data/matrix/notation): split into 2 files (#10199)

urkud committed 4 years ago

7d240ce1

feat(analysis/special_functions/log): Relating `log`-inequalities and `exp`-inequalities (#10191)

YaelDillies committed 4 years ago

daac8545

feat(algebra/group/with_one): cleanup algebraic instances (#10194)

eric-wieser committed 4 years ago

169bb29d

feat(analysis/normed_space/continuous_affine_map): define bundled continuous affine maps (#10161)

ocfnash committed 4 years ago

56a9228f

feat(algebra/homology/image_to_kernel): homology.map_iso (#9978)

jcommelin committed 4 years ago

26c0c23e

chore(algebra/opposites): use `injective.*` constructors (#10200)

urkud committed 4 years ago

f18278de

feat(data/nat/basic): `a < a / b * b + b` (#10193)

YaelDillies committed 4 years ago

38caa506

feat(algebra/big_operators/order): Bound on a product from a pointwise bound (#10190)

YaelDillies committed 4 years ago

ebe7951d

fix(README): update specialties of maintainers (#10086)

jcommelin committed 4 years ago

be412c3d

feat(data/set/equitable): A singleton is equitable (#10192)

YaelDillies committed 4 years ago

0c54c57c

chore(algebra/group/ulift): use injective.* to define instances (#10172)

urkud committed 4 years ago

af36f1a3

feat(data/fintype): instances for `infinite (α ⊕ β)` and `infinite (α × β)` (#10196)

urkud committed 4 years ago

4b14ef48

feat(data/list/basic): list products (#10184)

stuart-presnell committed 4 years ago

239bf055

feat(data/sym/sym2): Induction on `sym2` (#10189)

YaelDillies committed 4 years ago

051cb615

chore(set_theory/cardinal_ordinal): use notation ω (#10197)

urkud committed 4 years ago

4341fff2

feat(analysis/inner_product_space/rayleigh): Rayleigh quotient produces eigenvectors (#9840)

hrmacbeth committed 4 years ago

8174bd07

feat(order/lattice): add `inf_lt_sup` (#10178)

urkud committed 4 years ago

6cd6975d

feat(algebra/group/inj_surj): add `injective.monoid_pow` etc (#10152)

urkud committed 4 years ago

85f64207

feat(category_theory/limits/shapes/multiequalizer): Multi(co)equalizers (#10169)

adamtopaz committed 4 years ago

d69501f1

chore(*complex*): add a few simp lemmas (#10187)

urkud committed 4 years ago

cc59673b

feat(analysis/calculus/times_cont_diff): `equiv.prod_assoc` is smooth. (#10165)

ocfnash committed 4 years ago

a71bfdca

refactor(data/multiset/locally_finite): Generalize `multiset.Ico` to locally finite orders (#10031)

YaelDillies committed 4 years ago

d9a80ee9

feat(combinatorics/simple_graph): adding simple_graph.support and mem_support / support_mono lemmas (#10176)

arthurpaulino committed 4 years ago

5f5ce2b4

chore(linear_algebra/affine_space/affine_map): make `affine_map.coe_sub` true by definition (#10182)

ocfnash committed 4 years ago

8ac2fa06

refactor(measure_theory/integral/bochner): remove superfluous hypothesis (#10181)

fpvandoorn committed 4 years ago

b22a7c7e

feat(algebra/order/with_zero): add with_zero.linear_ordered_comm_grou… (#10180)

mariainesdff committed 4 years ago

88b4ce73

refactor(algebra/group): move `monoid.has_pow` etc to `algebra.group.defs` (#10147)

urkud committed 4 years ago

b31af6d9

Older