leanprover-community/mathlib

Pull Requests Commits

feat(data/fintype/basic): add fin_injective (#10330)

eric-wieser committed 4 years ago

65ff54c7

feat(linear_algebra/determinant): linear coordinates are ratio of determinants (#10261)

ocfnash committed 4 years ago

93047c52

feat(topology/homotopy/fundamental_groupoid): The functor from `Top` to `Groupoid` (#10195)

shingtaklam1324 committed 4 years ago

7ccc7ae6

feat(data/fintype): computable trunc bijection from fin (#10141)

kmill committed 4 years ago

9c03e9dc

feat(ring_theory/subring): weaken typeclass assumption for `units.pos_subgroup` (#10332)

ocfnash committed 4 years ago

7b607682

feat(data/pi): Composition of addition/subtraction/... of functions (#10305)

YaelDillies committed 4 years ago

7803884e

feat(category_theory/limits): Random results about limits. (#10285)

erdOne committed 4 years ago

43ef5787

feat(data/finset/basic): A finset has card two iff it's `{x, y}` for some `x ≠ y` (#10252)

YaelDillies committed 4 years ago

1a47cfc7

feat(category_theory/preadditive/additive_functor): map_zero' is a redundant field, remove it (#10229)

jcommelin committed 4 years ago

9fe0cbc8

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

Newer Older