leanprover-community/mathlib

Pull Requests Commits

some potentially useful WIP stuff

fpvandoorn committed 4 years ago

a715bb7e

ADedecker committed 4 years ago

35171ba8

fix(logic/basic): remove `noncomputable lemma` (#10292)

eric-wieser committed 4 years ago

64418d7e

chore(analysis/special_functions/trigonometric/arctan): put lemmas about derivatives into a new file (#10157)

RemyDegenne committed 4 years ago

d5d60719

feat(category_theory/sites/limits): `Sheaf J D` has colimits. (#10334)

adamtopaz committed 4 years ago

02100d81

feat(algebra/big_operators/basic): Sum over a product of finsets, right version (#10124)

YaelDillies committed 4 years ago

bf068540

feat(group_theory/group_action): add a few instances (#10310)

urkud committed 4 years ago

ca5c4b37

feat(order/sup_indep): Finite supremum independence (#9867)

YaelDillies committed 4 years ago

ca61dbff

feat(category_theory/sites/limits): `Sheaf_to_presheaf` creates limits (#10328)

adamtopaz committed 4 years ago

60bc370d

feat(category_theory/sites/sheafification): The sheafification of a presheaf. (#10303)

adamtopaz committed 4 years ago

189e0662

feat(analysis/inner_product_space/spectrum): more concrete diagonalization theorem (#10317)

hrmacbeth committed 4 years ago

62992fa9

feat(linear_algebra/trace): add lemmas about trace of linear maps (#10279)

antoinelab01 committed 4 years ago

0c8f53e5

feat(linear_algebra/alternating): add alternating_map.comp_linear_map (#10314)

eric-wieser committed 4 years ago

1b51fe0f

feat(measure_theory): drop some unneeded assumptions (#10319)

urkud committed 4 years ago

8728e85b

feat(data/equiv/module): add module.to_module_End (#10300)

eric-wieser committed 4 years ago

5307dc1b

chore(data/fin/basic): move tuple stuff to a new file (#10295)

eric-wieser committed 4 years ago

299af47c

feat(data/nat/basic): Some `nat.find` lemmas (#10263)

YaelDillies committed 4 years ago

7dc33bf7

feat(data/list/big_operators): When `list.sum` is strictly positive (#10282)

YaelDillies committed 4 years ago

dd72ebc0

feat(algebra/lie/basic): add missing `@[ext]` and `@[simp]` lemmas (#10316)

urkud committed 4 years ago

bca82787

refactor(set_theory/cardinal_ordinal): use TC assumptions instead of inequalities (#10313)

urkud committed 4 years ago

3b5edd06

feat(ring_theory,algebraic_geometry): Miscellaneous lemmas/def/typo corrections (#10307)

alreadydone committed 4 years ago

d8c87253

feat(measure_theory/group): define a few `measurable_equiv`s (#10299)

urkud committed 4 years ago

ca56c5ad

feat(*/{group,mul}_action): more lemmas (#10308)

urkud committed 4 years ago

3578403f

chore(data/equiv/*): rename `trans_symm` and `symm_trans` to `self_trans_symm` and `symm_trans_self`. (#10309)

eric-wieser committed 4 years ago

b91d3449

chore(measure_theory/probability_mass_function): Refactor the `pmf` file into a definitions file and a constructions file (#10298)

dtumad committed 4 years ago

869cb328

feat(linear_algebra/bilinear_form): add is_refl and ortho_sym for alt_bilin_form (#10304)

mcdoll committed 4 years ago

a7e38a03

feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an `orthogonal_family` (#10208)

hrmacbeth committed 4 years ago

a2323660

feat(category_theory/sites/plus): If P is a sheaf, then the map from P to P^+ is an isomorphism. (#10297)

adamtopaz committed 4 years ago

8bb0b6f7

feat(data/nat/basic): recursion for set nat (#10273)

stuart-presnell committed 4 years ago

55534c4f

feat(analysis/inner_product_space/spectrum): diagonalization of self-adjoint endomorphisms (finite dimension) (#9995)

hrmacbeth committed 4 years ago

6afda884

Older