Commits leanprover-community/mathlib3

refactor(tactic/*): mark internal attrs as `parser := failed` (#8635)

digama0 committed 4 years ago

c2580ebc

feat(analysis/convex/basic): add lemma add_smul regarding linear combinations of convex sets (#8608)

alexjbest committed 4 years ago

8a2a6304

feat(algebra/quaternion_basis): add a quaternion version of complex.lift (#8551)

eric-wieser committed 4 years ago

2412b97f

feat(ring_theory/dedekind_domain): ideals in a DD are cancellative (#8513)

Vierkantor committed 4 years ago

8914b68a

docs(data/fintype/sort): add module docstring (#8643)

YaelDillies committed 4 years ago

0f591415

feat(measure_theory/stieltjes_measure): Stieltjes measures associated to monotone functions (#8266)

sgouezel committed 4 years ago

3689655d

feat(measure_theory/vector_measure): a signed measure restricted on a positive set is a unsigned measure (#8597)

kex-y committed 4 years ago

7b27f461

feat(algebra/group_with_zero): `units.mk0` is a "monoid hom" (#8625)

Vierkantor committed 4 years ago

ee189957

feat(measure_theory/lp_space): add mem_Lp and integrable lemmas for is_R_or_C.re/im and inner product with a constant (#8615)

RemyDegenne committed 4 years ago

e17e9eac

feat(linear_algebra): Smith normal form for submodules over a PID (#8588)

Vierkantor committed 4 years ago

f63c27b0

feat(data/nat/prime, number_theory/padics/padic_norm): list of prime_pow_factors, valuation of prime power (#8473)

ineswright committed 4 years ago

e245b24b

feat(data/sym2): card of `sym2 α` (#8426)

YaelDillies committed 4 years ago

1b96e977

refactor(group_theory/sylow): make new file about actions of p groups and move lemmas there (#8595)

ChrisHughes24 committed 4 years ago

c550e3a3

feat(group_theory/subgroup): there are finitely many subgroups of a finite group (#8593)

ChrisHughes24 committed 4 years ago

0cbab378

chore(measure_theory/*): make measurable_space arguments implicit, determined by the measure argument (#8571)

RemyDegenne committed 4 years ago

cd2b5495

doc(tactic/cache): fix haveI docs (#8637)

digama0 committed 4 years ago

9ab4d281

fix(tactic/lint): _ is not a linter (#8634)

digama0 committed 4 years ago

036c96bf

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

leanprover-community-bot committed 4 years ago

89687399

feat(analysis/normed_space/finite_dimension): asymptotic equivalence preserves summability (#8596)

ADedecker committed 4 years ago

f0ae67d0

feat(tactic/cache): allow optional := in haveI (#8631)

digama0 committed 4 years ago

ea7e3ff7

refactor(tactic/tidy): use @[user_attribute] (#8630)

digama0 committed 4 years ago

565fef65

feat(data/equiv/basic): add a small lemma for simplifying map between equivalent quotient spaces induced by equivalent relations (#8617)

Paul-Lez committed 4 years ago

7b5c60db

chore(group_theory/group_action/defs): add a missing is_scalar_tower instance (#8604)

eric-wieser committed 4 years ago

3ebf9f08

feat(group_theory/perm/cycle_type): purge trunc references (#8176)

pechersky committed 4 years ago

2489931e

chore(group_theory/submonoid/membership): missing rfl lemmas (#8619)

eric-wieser committed 4 years ago

2db8c799

feat(data/rat/basic): Add nat num and denom inv lemmas (#8581)

FrickHazard committed 4 years ago

8d0ed030

feat(analysis/normed_space): controlled surjectivity (#8498)

PatrickMassot committed 4 years ago

1d4400c1

refactor(measure_theory): add subfolder (#8594)

fpvandoorn committed 4 years ago

9c8602b0

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

leanprover-community-bot committed 4 years ago

6305769a

docs(data/set/lattice): add module docstring (#8250)

YaelDillies committed 4 years ago

3c09987c