leanprover-community/mathlib

Pull Requests Commits

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

adamtopaz committed 4 years ago

189e0662

urkud committed 4 years ago

37c11e4a

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

hrmacbeth committed 4 years ago

62992fa9

urkud committed 4 years ago

13f440aa

urkud committed 4 years ago

ed6696b6

urkud committed 4 years ago

b926ade6

Merge branch 'master' into YK-integral-meas-pres

urkud committed 4 years ago

dca91a5f

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

Docs, use measures

urkud committed 4 years ago

b6f3c201

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

urkud committed 4 years ago

0f7a8822

Merge branch 'master' into YK-smul-inv-meas

urkud committed 4 years ago

82e698dc

Merge branch 'YK-minimal-action' into YK-smul-inv-meas

urkud committed 4 years ago

9a6f36cc

Merge branch 'YK-regular-transitive' into YK-minimal-action

urkud committed 4 years ago

b6d2247d

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

urkud committed 4 years ago

3b5edd06

urkud committed 4 years ago

fd64632e

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

alreadydone committed 4 years ago

d8c87253

Merge branch 'YK-grp-action' into YK-regular-transitive

urkud committed 4 years ago

56efb5c9

Merge branch 'master' into YK-grp-action

urkud committed 4 years ago

29faa06d

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

urkud committed 4 years ago

b2a053f9

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

feat(group_theory/group_action): add a few instances

urkud committed 4 years ago

1ceb4274

Newer Older