leanprover-community/mathlib3

Pull Requests Commits

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

feat(archive/imo): IMO 2001 Q6 (#8327)

saradiazr11 committed 4 years ago

694dd117

feat(measure_theory/measure_space): add mutually singular measures (#8605)

kex-y committed 4 years ago

32735ca2

feat(measure_theory/l2_space): generalize inner_indicator_const_Lp_one from R to is_R_or_C (#8602)

RemyDegenne committed 4 years ago

3b279c17

feat(analysis/normed_space/inner_product): add norm_inner_le_norm (#8601)

RemyDegenne committed 4 years ago

d1b2a548

feat(algebra/pointwise): add preimage_smul and generalize a couple of assumptions (#8600)

alexjbest committed 4 years ago

acab4f94

chore(analysis/calculus/fderiv_symmetric): Squeeze some simps in a very slow proof (#8609)

eric-wieser committed 4 years ago

9fb53f98

feat(measure_theory/special_functions): add measurability of is_R_or_C.re and is_R_or_C.im (#8603)

RemyDegenne committed 4 years ago

ebe01764

chore(linear_algebra/quadratic_form): make Sylvester's law of inertia bold in the doc string (#8610)

kex-y committed 4 years ago

57391993

fix(docs/references.bib): add missing comma (#8585)

mans0954 committed 4 years ago

e2b7f706

Newer Older