leanprover-community/mathlib

Pull Requests Commits

Undo rename in `test/elementwise.lean`

Vierkantor committed 4 years ago

4c51e75f

Fix timeout due to elaborator confusion

Vierkantor committed 4 years ago

5b154e45

Instantiate `add_monoid_hom_class` for `continuous_linear_map`

Vierkantor committed 4 years ago

ef7e8ddd

Fix `field_theory/finite/galois_field.lean` (name confusion)

Vierkantor committed 4 years ago

8ffb4d02

Fix `ring_theory/derivation.lean` (simp normal form, help the elaborator)

Vierkantor committed 4 years ago

52b64a6b

Merge branch 'master' into fun_like

YaelDillies committed 4 years ago

Verified 5a2f70ae

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

Older