leanprover-community/mathlib

Pull Requests Commits

feat(data/nat/digits): add norm_digits tactic (#4452)

digama0 committed 5 years ago

952a407c

feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem (#4407)

hrmacbeth committed 5 years ago

b1ca33e0

feat(analysis/normed_space/inner_product): Cauchy-Schwarz equality case and other lemmas (#4571)

dupuisf committed 5 years ago

b48b4ff0

chore(linear_algebra/finite_dimensional): rename `of_finite_basis` (#4562)

urkud committed 5 years ago

0f085b98

chore(*): assorted lemmas (#4566)

urkud committed 5 years ago

14dcfe0c

chore(data/finsupp): replace `eq_zero_of_zero_eq_one` with `finsupp.unique_of_right` (#4563)

urkud committed 5 years ago

918e5d82

chore(measure_theory/measurable_space): add `finset.is_measurable_bUnion` etc (#4553)

urkud committed 5 years ago

33f7870a

chore(algebra/monoid_algebra): Reorder lemmas, name some sections for clarity (#4535)

eric-wieser committed 5 years ago

99130d84

chore(algebra/algebra/basic): fix definition of `ring_hom.to_algebra` (#4561)

urkud committed 5 years ago

0487a1d2

chore(order/well_founded): move to a file (#4568)

urkud committed 5 years ago

2c53e5ee

chore(scripts): update nolints.txt (#4564)

leanprover-community-bot committed 5 years ago

4dbebe3b

feat(data/finset/basic): equivalence of finsets from equivalence of types (#4560)

b-mehta committed 5 years ago

d8d6e18c

chore(topology/*): golf some proofs (#4528)

urkud committed 5 years ago

df5adc5c

feat(data/equiv/basic): equivalence on functions from bool (#4559)

b-mehta committed 5 years ago

c726898e

feat(data/finset/pi): pi singleton lemmas (#4558)

b-mehta committed 5 years ago

f91e0c68

feat(topology/uniform_space/cauchy): generalize `second_countable_of_separable` to uniform spaces (#4530)

urkud committed 5 years ago

c8738cb6

feat(analysis/special_functions/*): a few more simp lemmas (#4550)

urkud committed 5 years ago

6676917e

chore(scripts): update nolints.txt (#4556)

leanprover-community-bot committed 5 years ago

b084a068

feat(measure_theory): additions (#4324)

fpvandoorn committed 5 years ago

40b55c0b

feat(ring_theory/power_series): inverse lemmas (#4552)

b-mehta committed 5 years ago

d533e1ce

feat(topology/basic): Lim_spec etc. cleanup (#4545)

adamtopaz committed 5 years ago

b167809a

feat(meta/expr): add parser for generated binder names (#4540)

JLimperg committed 5 years ago

fcaf6e91

chore(algebra/big_operators/basic): add lemma prod_multiset_count' that generalize prod_multiset_count to consider a function to a monoid (#4534)

riccardobrasca committed 5 years ago

306dc8a0

chore(topology/instances/nnreal): use notation (#4548)

urkud committed 5 years ago

656ef0a5

lint(various): nolint has_inhabited_instance for injective functions (#4541)

hrmacbeth committed 5 years ago

d0f45f52

chore(data/nat/cast): a few `simp`/`norm_cast` lemmas (#4549)

urkud committed 5 years ago

cc75e4ef

Merge branch 'ordered_semiring_zero_le_one' into bell

kim-em committed 5 years ago

c709dede

kim-em committed 5 years ago

c2572d57

chore(scripts): update nolints.txt (#4547)

leanprover-community-bot committed 5 years ago

f6836c16

chore(topology/algebra/group): move a lemma to `group_theory/coset` (#4522)

urkud committed 5 years ago

8004fb68

Newer Older