leanprover-community/mathlib

Pull Requests Commits

simplify proof of exp_bound'

isadofschi committed 4 years ago

23da4531

Apply suggestions from code review

isadofschi committed 4 years ago

Verified 2828a11b

isadofschi committed 4 years ago

cec8a100

Apply suggestions from code review

isadofschi committed 4 years ago

Verified 70ccb66f

tidy more following suggestions from code review

isadofschi committed 4 years ago

34df5d80

Apply suggestions from code review

isadofschi committed 4 years ago

Verified 2d7765b3

split long docstring into two lines

isadofschi committed 4 years ago

74897322

isadofschi committed 4 years ago

6e587c09

rename new lemmas

isadofschi committed 4 years ago

48372ca1

feat(add_one_le_exp): add lemma add_one_le_exp

isadofschi committed 4 years ago

2ae30fad

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

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

Older