leanprover-community/mathlib3

Pull Requests Commits

AlexKontorovich committed 4 years ago

c986b483

AlexKontorovich committed 4 years ago

c2e949df

something1 is almost done

AlexKontorovich committed 4 years ago

7986bcd6

AlexKontorovich committed 4 years ago

4cc31a7d

AlexKontorovich committed 4 years ago

24282d37

real_to_haar2 progress

AlexKontorovich committed 4 years ago

cd977f9e

AlexKontorovich committed 4 years ago

f4f6a263

AlexKontorovich committed 4 years ago

e8623135

AlexKontorovich committed 4 years ago

89244d7d

AlexKontorovich committed 4 years ago

8dbdb1d7

auto_descend hell

AlexKontorovich committed 4 years ago

665ac2ce

AlexKontorovich committed 4 years ago

617dde7f

feat(field_theory): more general `algebra _ (algebraic_closure k)` instance (#8658)

Vierkantor committed 4 years ago

8eca2934

feat(linear_algebra/basic, group_theory/quotient_group, algebra/lie/quotient): ext lemmas for morphisms out of quotients (#8641)

eric-wieser committed 4 years ago

c711909c

feat(data/list/perm): subperm_ext_iff (#8504)

pechersky committed 4 years ago

9e83de22

chore(*): update lean to 3.32.1 (#8652)

digama0 committed 4 years ago

733e6e34

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

Older