leanprover-community/mathlib

Pull Requests Commits

feat(tactic/extract_goal): improve formatting to put assumptions on their own line (#2076)

cipher1024 committed 6 years ago

Verified 13f04c00

feat(topology/metric_space/antilipschitz): define `antilipschitz_with` (#2075)

urkud committed 6 years ago

Verified 545dd03d

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

02d22c39

feat(tactic/lint): check for redundant simp lemmas (#2066)

gebner committed 6 years ago

Verified f7e82d06

fix some docstrings [ci skip] (#2078)

fpvandoorn committed 6 years ago

Verified 2d1bd457

feat(data/list/basic): more lemmas about `list.chain'`; `chain'_of_pairwise` → `pairwise.chain'` (#2071)

urkud committed 6 years ago

Verified 2a9ad03c

feat(analysis/calculus/iterated_deriv): iterated derivative of a function defined on the base field (#2067)

sgouezel committed 6 years ago

Verified e0030149

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

262a39ef

feat(tactic/nat_cases): a tactic to case bash inequalities on natural numbers (#1596)

kim-em committed 6 years ago

Verified fe9d7ff4

doc(data/fin): add docs; fin_zero_elim -> fin.elim0; fin_zero_elim' -> fin_zero_elim (#2055)

urkud committed 6 years ago

Verified 1d82a7c2

feat(data/finset): new basic material on finsets and fintypes (#2068)

sgouezel committed 6 years ago

Verified 8919541a

chore(data/real/ennreal): weaker assumptions in `sub_mul`, add `coe_inv_le` (#2074)

urkud committed 6 years ago

Verified 62756bd3

chore(algebra/group): move `is_mul/monoid/group_hom` to `deprecated/` (#2056)

urkud committed 6 years ago

Verified bfbd0937

chore(topology/metric_space/isometry): rename `(e)metric.isometry.diam_image` to `isometry.(e)diam_image` (#2073)

urkud committed 6 years ago

Verified 3055b3c0

feat(order/galois_connection): lemmas about galois insertions and supr/infi (#2052)

jcommelin committed 6 years ago

Verified 2683fa09

feat(algebra/free_monoid): define `lift` and `map`, move out of `algebra/group` (#2060)

urkud committed 6 years ago

Verified d5d907b1

fix(.mergify.yml): remove " (leanprover-community/lean:3.5.1)" (#2077)

urkud committed 6 years ago

Verified aec54b3b

fix(tactic/omega): reify nonconstant ints and nats (#1748)

skbaek committed 6 years ago

19a9bdc2

chore(ci): remove unneeded Lean version restrictions (#2065)

robertylewis committed 6 years ago

Verified 354a4ed1

feat(ring_theory): Fractional ideals (#2062)

Vierkantor committed 6 years ago

Verified 07608293

fix(tactic/ring): more precise pattern match for div (#1557)

digama0 committed 6 years ago

Verified 4149099c

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

0bf20640

refactor(analysis/calculus/times_cont_diff): massive refactor (#2012)

sgouezel committed 6 years ago

Verified 4637e5c8

feat(ci): avoid push to Azure if branch has been updated (#2048)

robertylewis committed 6 years ago

Verified 0e4eb09d

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

691456c6

feat(tactic/tidy): include norm_cast in tidy (#2063)

kim-em committed 6 years ago

Verified 7907f8f3

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

6c2411bd

doc(data/finsupp): module docs and docstrings (#2059)

bryangingechen committed 6 years ago

Verified a46b3e57

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

ef1e38ec

feat(ring_theory/polynomial): mv_polynomial.integral_domain (#2021)

jcommelin committed 6 years ago

Verified f0bb2f82

Newer Older