leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/normed_space/*): group of units of a normed ring is open (#3210)

hrmacbeth committed 5 years ago

0d249d70

fix(tactic/default): import tactic.basic (#3284)

bryangingechen committed 5 years ago

c2886d31

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

leanprover-community-bot committed 5 years ago

2a43e26f

feat(ring_theory/polynomial): rational root theorem and integral root theorem (#3241)

Vierkantor committed 5 years ago

742dc887

chore(algebra/ordered_group): deduplicate (#3279)

urkud committed 5 years ago

c4bf9e44

feat(field_theory/splitting_field): definition of splitting field (#3272)

kckennylau committed 5 years ago

f1637e56

feat(algebra/pointwise): make instances global (#3240)

fpvandoorn committed 5 years ago

48dea2fd

feat(analysic/calculus/times_cont_diff): add times_cont_diff_within_at (#3262)

sgouezel committed 5 years ago

f9f0ca6d

feat(geometry/manifold/smooth_manifold_with_corners): product of smooth manifolds with corners (#3250)

Nicknamen committed 5 years ago

53c15319

chore(order/filter/basic): implicit arg in `eventually_of_forall` (#3277)

urkud committed 5 years ago

e236160f

fix(algebra/group_with_zero): fix left/right (#3278)

urkud committed 5 years ago

56ed551e

feat(category_theory/abelian): every abelian category is preadditive (#3247)

TwoFX committed 5 years ago

303740d4

chore(*): reduce imports (#3235)

kim-em committed 5 years ago

9b086e10

feat(category_theory/limits): fully faithful functors reflect limits and colimits (#3269)

b-mehta committed 5 years ago

6a49975f

feat(topology/basic): add `eventually_eventually_nhds` (#3266)

urkud committed 5 years ago

838dc66e

feat(data/real/cardinality): cardinalities of intervals of reals (#3252)

jsm28 committed 5 years ago

d84c48c8

refactor(analysis/calculus/*deriv): use eventually_eq in congruence statements (#3261)

sgouezel committed 5 years ago

e4fdc750

feat(analysis/specific_limits): proof of harmonic series diverging and preliminaries (#3233)

ADedecker committed 5 years ago

237b1ea5

fix(library_search): fix a bug with iff lemmas where both sides match (#3270)

kim-em committed 5 years ago

8be66ee9

chore(tactic/noncomm_ring): allow simp to fail (#3268)

kim-em committed 5 years ago

18a80ea2

feat(data/polynomial): preliminaries for Cayley-Hamilton (#3243)

kim-em committed 5 years ago

dc1d9369

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

leanprover-community-bot committed 5 years ago

cd29ede9

chore(algebra/*): deduplicate `*_with_zero`/`semiring`/`field` (#3259)

urkud committed 5 years ago

93099107

feat(data/nat/digits): add digits_lt_base (#3246)

kbuzzard committed 5 years ago

1a419a9f

chore(*): work on removing deprecated is_X_hom typeclasses (#3258)

kim-em committed 5 years ago

f00b7c0c

feat(field_theory/separable): relating irreducibility and separability (#3198)

kckennylau committed 5 years ago

e803c851

chore(data/set/basic): simp attribute on mem_range_self (#3260)

sgouezel committed 5 years ago

a7cdab5d

chore(data/finset, data/multiset): split into smaller files (#3256)

kim-em committed 5 years ago

7bd19b32

feat(category/preadditive): properties of preadditive biproducts (#3245)

kim-em committed 5 years ago

8ba7595a

chore(algebra/big_operators): don't use omega (#3255)

kim-em committed 5 years ago

aff951a5

Newer Older