leanprover-community/mathlib

Pull Requests Commits

chore(measure_theory/measure/hausdorff): golf (#8706)

urkud committed 4 years ago

edb0ba42

feat(ring_theory/fractional_ideal): lemmas on `span_singleton _ x * I` (#8624)

Vierkantor committed 4 years ago

0591c276

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

leanprover-community-bot committed 4 years ago

b6f1214f

chore(data/nat/pairing): add `pp_nodot`, fix some non-finalizing `simp`s (#8705)

urkud committed 4 years ago

1263906f

chore(analysis/calculus/deriv): weaker assumptions for `deriv_mul_const` (#8704)

urkud committed 4 years ago

40d2602e

chore(data/vector): rename vector2 (#8697)

eric-wieser committed 4 years ago

d5ce7e56

feat(ring_theory/ideal): lemmas on `ideal.span {x} * I` (#8622)

Vierkantor committed 4 years ago

253712e1

feat(ring_theory/localization): some lemmas on `coe_submodule` (#8621)

Vierkantor committed 4 years ago

65b0c582

chore(ring_theory): generalize `non_zero_divisors` lemmas to `monoid_with_zero` (#8607)

Vierkantor committed 4 years ago

80b699bc

feat(group_theory/nilpotent): add nilpotent groups (#8538)

kbuzzard committed 4 years ago

106bd3be

feat(data/fintype/basic): card_sum, card_subtype_or (#8490)

pechersky committed 4 years ago

a55084f5

feat(algebra/big_operators/basic): prod_subsingleton (#8423)

pechersky committed 4 years ago

f8241b74

feat(finsupp/basic): lemmas about emb_domain (#7883)

kim-em committed 4 years ago

e1953471

puzzle(archive/oxford_invariants): Oxford Invariants Puzzle Challenges, Summer 2021, Week 3, Problem 1 (#8656)

YaelDillies committed 4 years ago

53d97e1a

feat(analysis/normed_space): normed group hom completion (#8499)

PatrickMassot committed 4 years ago

55b2e864

feat(analysis): `x^y` is smooth as a function of `(x, y)` (#8262)

urkud committed 4 years ago

217308c9

feat(tactic/abel): check for defeq of atoms instead of syntactic eq (#8628)

Vierkantor committed 4 years ago

d6aae6c6

feat(algebra/lie/semisimple): adjoint action is injective for semisimple Lie algebras (#8698)

ocfnash committed 4 years ago

deedf250

feat(algebra/gcd_monoid): move the `gcd_monoid nat` instance (#7180)

Julian-Kuelshammer committed 4 years ago

c416a486

feat(measure_theory/hausdorff_measure): Hausdorff measure and volume coincide in pi types (#8554)

sgouezel committed 4 years ago

2b435875

fix(*): fix universe levels (#8677)

fpvandoorn committed 4 years ago

a983f241

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

leanprover-community-bot committed 4 years ago

69785fe0

chore(algebra/module): Swap the naming of `smul_(left|right)_injective` to match the naming guide (#8659)

eric-wieser committed 4 years ago

b97344c0

feat(tactic/ext): add tracing option (#8633)

robertylewis committed 4 years ago

2e9029fe

docs(data/pfun): add module docstring and def docstrings (#8629)

YaelDillies committed 4 years ago

59954c19

feat(topology/category/*/projective): CompHaus and Profinite have enough projectives (#8613)

jcommelin committed 4 years ago

46b3fae0

feat(algebraic_geometry/EllipticCurve): add working definition of elliptic curve (#8558)

kbuzzard committed 4 years ago

4bf51778

feat(set_theory/cardinal): lift_sup (#8675)

kim-em committed 4 years ago

ec68c7e4

feat(measure): prove Haar measure = Lebesgue measure on R (#8639)

fpvandoorn committed 4 years ago

462359db

chore(analysis/normed_space/dual): golf some proofs (#8694)

hrmacbeth committed 4 years ago

8e508633

Newer Older