leanprover-community/mathlib

Pull Requests Commits

restore some comments

alexjbest committed 4 years ago

b68daba6

revert random line change

alexjbest committed 4 years ago

72dee86a

Merge branch 'master' of github.com:leanprover-community/mathlib into alexjbest/imports/sed6

alexjbest committed 4 years ago

f1d45fe3

chore(order/filter/basic): add 2 trivial `simp` lemmas (#10344)

urkud committed 4 years ago

f01399c4

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

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

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

ocfnash committed 4 years ago

9264f302

alexjbest committed 4 years ago

0f6df534

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

alexjbest committed 4 years ago

1bf30c46

alexjbest committed 4 years ago

f84ef277

alexjbest committed 4 years ago

5f37cd1d

Merge branch 'master' of github.com:leanprover-community/mathlib into alexjbest/imports/sed6

alexjbest committed 4 years ago

0593d0c8

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

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

Older