leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 5 years ago

dda5c0c5

kim-em committed 5 years ago

21ff1614

kim-em committed 5 years ago

a387c004

kim-em committed 5 years ago

06fc15df

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

kim-em committed 5 years ago

97d3ed15

Merge branch 'hom_equiv_2' of github.com:leanprover-community/mathlib into hom_equiv_2

kim-em committed 5 years ago

37ce8864

kim-em committed 5 years ago

37ee0ba4

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

urkud committed 5 years ago

Verified 1d82a7c2

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

sgouezel committed 5 years ago

Verified 8919541a

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

urkud committed 5 years ago

Verified 62756bd3

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

urkud committed 5 years ago

Verified bfbd0937

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

urkud committed 5 years ago

Verified 3055b3c0

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

jcommelin committed 5 years ago

Verified 2683fa09

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

urkud committed 5 years ago

Verified d5d907b1

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

urkud committed 5 years ago

Verified aec54b3b

Apply suggestions from code review

kim-em committed 5 years ago

Verified 5c06b435

Apply suggestions from code review

kim-em committed 5 years ago

Verified b81222e4

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

skbaek committed 5 years ago

19a9bdc2

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

robertylewis committed 5 years ago

Verified 354a4ed1

feat(ring_theory): Fractional ideals (#2062)

Vierkantor committed 5 years ago

Verified 07608293

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

digama0 committed 5 years ago

Verified 4149099c

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

0bf20640

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

sgouezel committed 5 years ago

Verified 4637e5c8

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

robertylewis committed 5 years ago

Verified 0e4eb09d

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

691456c6

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

kim-em committed 5 years ago

Verified 7907f8f3

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

6c2411bd

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

bryangingechen committed 5 years ago

Verified a46b3e57

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

ef1e38ec

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

jcommelin committed 5 years ago

Verified f0bb2f82

Older