leanprover-community/mathlib

Pull Requests Commits

feat(ring_theory/ideal_over): a prime ideal lying over a maximal ideal is maximal (#3488)

Vierkantor committed 6 years ago

d974457e

chore(data/sym2) : simplify proofs (#3522)

jalex-stark committed 6 years ago

7397db78

chore(topology/uniform_space/basic): golf a proof (#3521)

urkud committed 6 years ago

c1498391

chore(order/complete_lattice): add `supr/infi_of_empty(')` (#3519)

urkud committed 6 years ago

4a918fbb

feat(analysis/convex/basic): add lemmas about convex combination of endpoints of intervals (#3482)

dupuisf committed 6 years ago

827fcd06

chore(data/subtype,order/complete_lattice): use `coe` instead of `subtype.val` (#3518)

urkud committed 6 years ago

fbcd8908

refactor(data/polynomial): re-organizing (#3512)

kim-em committed 6 years ago

1dd69d30

chore(*): cleanup imports (#3511)

kim-em committed 6 years ago

36ea9e84

feat(data/nat/digits): a number is bigger than base^(digits length - 1) (#3498)

SnobbyDragon committed 6 years ago

a8cedf9f

feat(tactic/extract_goal): remove annoying spaces (#3514)

cipher1024 committed 6 years ago

acc2802d

refactor(linear_algebra/nonsingular_inverse, data/matrix/basic): update_* rectangular matrices (#3403)

pechersky committed 6 years ago

a971a88f

feat(category_theory/kernels): compute kernel (f ≫ g) when one is an iso (#3438)

kim-em committed 6 years ago

90d33863

refactor(algebra/big_operators): split file, reduce imports (#3495)

kim-em committed 6 years ago

39f8f020

feat(tactic/extract_goal): better support for `let` expressions (#3496)

cipher1024 committed 6 years ago

197b5015

chore(topology/category/): switch to bundled morphisms in Top (#3506)

kim-em committed 6 years ago

64335dec

feat(data/list/basic): induction from both ends (#3448)

lambda-fairy committed 6 years ago

dced3436

fix(ring_theory/jacobson): Clean up documentation in Jacobson Ring definitions (#3501)

dtumad committed 6 years ago

55e7dcc1

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

leanprover-community-bot committed 6 years ago

314b2094

feat(tactic/linarith): put certificate generation in tactic monad (#3504)

robertylewis committed 6 years ago

2219dc18

feat(ring_theory/discrete_valuation_ring): add DVR (#3476)

kbuzzard committed 6 years ago

219e2981

fix(algebra/ring): add coe_neg_one lemma to units (#3489)

alexpeattie committed 6 years ago

84d64972

feat(tactic/linarith): modularize coefficient oracle (#3502)

robertylewis committed 6 years ago

e448bb1a

feat(algebra/invertible): invertible elements are units (#3499)

Oliver Nash committed 6 years ago

c6aa8e72

feat(group_theory/semidirect_product): semidirect_product.map (#3492)

ChrisHughes24 committed 6 years ago

2fb6a056

chore(analysis/special_functions): moved trig vals out of real.pi, added new trig vals (#3497)

benjamindavidson committed 6 years ago

dfef07a8

feat(data/{mv_}polynomial): make args to aeval implicit (#3494)

robertylewis committed 6 years ago

c47d1d0d

feat(algebra/invertible): lemmas (#3493)

robertylewis committed 6 years ago

7efdd990

feat(topology): more lemmas about Ici and Iic neighborhoods (#3474)

ADedecker committed 6 years ago

5776f4c0

feat(topology): implemented continuous bundled maps (#3486)

Nicknamen committed 6 years ago

49049e46

kim-em committed 6 years ago

a67edbf0

Newer Older