leanprover-community/mathlib3

Pull Requests Commits

Scott Morrison committed 5 years ago

21e615a3

Merge remote-tracking branch 'origin/master' into HEAD

ChrisHughes24 committed 5 years ago

586b13cb

fix(algebra/punit_instance): punit.smul_eq is marked simp and can be proved by simp (#2291)

ChrisHughes24 committed 5 years ago

Verified 8a617238

Merge branch 'master' into group_ring_lemmas

mergify[bot] committed 5 years ago

Verified 52dfdeee

doc(algebra/group/type_tags): add docs (#2287)

urkud committed 5 years ago

Verified 3f0e700c

chore(*): completing most of the -T50000 challenge (#2281)

kim-em committed 5 years ago

Verified 1331e29b

feat(data/fin*): uniqueness of increasing bijection (#2258)

sgouezel committed 5 years ago

Verified 37212a78

docs(algebraic_geometry/prime_spectrum): linkify url in module docs (#2288)

jcommelin committed 5 years ago

Verified cd38923e

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

9288d10e

chore(data/set/lattice): use dot syntax for `disjoint.*` (#2282)

urkud committed 5 years ago

Verified 51553e36

chore(*): remove 'using_well_founded wf_tacs', fixed in core (#2280)

kim-em committed 5 years ago

Verified cf648606

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

8c1e32f3

feat(ci): try fetching olean caches from older commits (#2278)

bryangingechen committed 5 years ago

Verified 7dad872f

chore(topology/algebra/ordered): `le_of_tendsto`: use `∀ᶠ`, add primed versions (#2270)

urkud committed 5 years ago

Verified c14c84e4

fix(tactic/squeeze): make suggestion at correct location (#2279)

gebner committed 5 years ago

Verified 8b679d98

feat(tactic/core): basic interaction monad functions (#1658)

khoek committed 5 years ago

Verified 38544f14

fix(tactic/core): remove all_goals option from apply_any (#2275)

kim-em committed 5 years ago

Verified c4fb4035

chore(data/opposite): two trivial lemmas (#2274)

urkud committed 5 years ago

Verified da8b23f9

chore(data/fintype/intervals): `simp` `Ico_*_card` lemmas (#2271)

urkud committed 5 years ago

Verified 79880e86

feat(analysis/calculus/fderiv): define `has_strict_fderiv_at` (#2249)

urkud committed 5 years ago

Verified 5d9e7f58

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

de8c2078

doc(ring_theory/noetherian): add docstring, normalise notation (#2219)

kbuzzard committed 5 years ago

Verified 8454c108

feat(category/equiv_functor): type-level functoriality w.r.t. equiv (#2255)

kim-em committed 5 years ago

Verified ecdb1383

feat(algebra/big_operators): missing lemmas (#2259)

sgouezel committed 5 years ago

Verified d500210b

feat(tactic/solve_by_elim): add accept parameter to prune tree search (#2245)

kim-em committed 5 years ago

Verified ad53e0b7

fix(scripts/deploy_docs.sh): cd before git log (#2264)

bryangingechen committed 5 years ago

Verified 0187cb57

chore(data/equiv/basic): simp to_fun to coe (#2256)

kim-em committed 5 years ago

Verified 17f83409

fix(tactic/squeeze): do not fail when closing the goal (#2262)

cipher1024 committed 5 years ago

Verified d470ae77

feat(analysis/normed_space/operator_norm): a few more estimates (#2233)

urkud committed 5 years ago

Verified 67327881

remove redundant lemmas

kim-em committed 5 years ago

7ff5a66f

Older