leanprover-community/mathlib

Pull Requests Commits

Update src/tactic/chain_trans.lean

cipher1024 committed 5 years ago

Verified 3588dd3e

Update chain_trans.lean

cipher1024 committed 5 years ago

Verified bf2109db

improve documentation

cipher1024 committed 5 years ago

96746725

remove unneeded total order

cipher1024 committed 5 years ago

2b24c687

sort edges to prioritize stronger proofs while avoiding exponential blowup

cipher1024 committed 5 years ago

ae0fac1b

break long lines

cipher1024 committed 5 years ago

c118626b

make semantics clearer and remove reference

cipher1024 committed 5 years ago

5287b4ab

discard proofs of \le when looking for proofs of \lt

cipher1024 committed 5 years ago

740af1e7

cipher1024 committed 5 years ago

5c320594

feat(tactic/chain_trans): prove inequalities by transitivity on multiple assumptions

cipher1024 committed 5 years ago

da9e1936

chore(topology/algebra/group): review (#4570)

urkud committed 5 years ago

665cc13c

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

Older