leanprover-community/mathlib

Pull Requests Commits

feat(algebra/order/archimedean): upgrade some `∃` to `∃!` (#10343)

urkud committed 4 years ago

1181c990

chore(*): clean up some unused open statements and extra simps (#10342)

alexjbest committed 4 years ago

30abde68

urkud committed 4 years ago

842feb99

feat(data/fin/basic): extract `div_nat` and `mod_nat` from `fin_prod_fin_equiv` (#10339)

eric-wieser committed 4 years ago

979f0e83

chore(ring_theory/subring): fix stale docstring (#10340)

ocfnash committed 4 years ago

bd80b339

urkud committed 4 years ago

b3cba98d

feat(analysis/calculus/times_cont_diff): continuous affine maps are smooth (#10335)

ocfnash committed 4 years ago

9264f302

feat(data/nat/lattice): add ```Inf_add``` lemma (#10008)

SymmetryUnbroken committed 4 years ago

bff69c9f

feat(algebra/homology/exact): preadditive.exact_iff_exact_of_iso (#9979)

jcommelin committed 4 years ago

ddb6c75f

chore(linear_algebra/pi_tensor_product): add reindex_reindex (#10336)

eric-wieser committed 4 years ago

90740956

feat(logic/relation): induction principles for `trans_gen` (#10331)

fpvandoorn committed 4 years ago

a0f2c47f

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

urkud committed 4 years ago

c5ce6ffc

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

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

urkud committed 4 years ago

d557c32c

urkud committed 4 years ago

c58f6d27

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

Newer Older