Commits leanprover-community/mathlib3

feat(finsupp/basic): restrict a finitely supported function on option A to A (#8342)

kim-em committed 4 years ago

03ddb8dd

feat(linear_algebra/invariant_basis_number): basic API lemmas (#7882)

kim-em committed 4 years ago

d0804bae

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

leanprover-community-bot committed 4 years ago

3b37614c

fix(tactic/core): mk_simp_attribute: remove superfluous disjunct (#8648)

digama0 committed 4 years ago

4a864ed0

feat(data/nat/(basic, modeq)): simple lemmas (#8647)

YaelDillies committed 4 years ago

ce26133b

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