leanprover-community/mathlib

Pull Requests Commits

Improved dot notation, hopefully more readable like this.

kkytola committed 4 years ago

4cc6f917

A misprint correction and a small golf.

kkytola committed 4 years ago

4db5a327

Inhabiting instances.

kkytola committed 4 years ago

d57bc8a4

Some renaming for better dot notation.

kkytola committed 4 years ago

850df5f8

Some cleaning up, especially dot notation.

kkytola committed 4 years ago

b3e50353

Fixing more too long doc-string lines almost right away.

kkytola committed 4 years ago

e56755ff

Fixing too long doc-string lines right away.

kkytola committed 4 years ago

83a7d961

Trying to fix missing def-doc-strings, retrying to fix (most) unused arguments, removing simp-tags.

kkytola committed 4 years ago

f87cea21

Trying to fix unused arguments by introducing variables. Order of lemmas changed. Also trying to fix simp normal form.

kkytola committed 4 years ago

39ca9a63

Update src/measure_theory/weak_convergence.lean

kkytola committed 4 years ago

Verified 3c145a6a

Fixing some more too long lines.

kkytola committed 4 years ago

1f75e36a

Fixing too long lines.

kkytola committed 4 years ago

eb29dc6d

feat(measure_theory/weak_convergence): define weak convergence of finite Borel measures

kkytola committed 4 years ago

1a7407d5

docs(measure_theory/integral_eq_improper): fix lemma names in docs (#8333)

ADedecker committed 4 years ago

10975e6d

feat(measure_theory/continuous_map_dense): continuous functions are dense in Lp (#8306)

hrmacbeth committed 4 years ago

8e3d9cee

chore(ring_theory/fractional_ideal): prefer `(⊤ : ideal R)` over `1` (#8298)

Vierkantor committed 4 years ago

a895300a

chore(linear_algebra/linear_independent): use `is_empty ι` instead of `¬nonempty ι` (#8331)

eric-wieser committed 4 years ago

42f7ca0f

feat(topology/metric_space/holder): define Hölder continuity (#8309)

urkud committed 4 years ago

9061ecc1

chore(topology/algebra/infinite_sum): relax the requirements on `has_sum.smul` (#8312)

eric-wieser committed 4 years ago

35a8d935

chore(set_theory/*): use `is_empty α` instead of `¬nonempty α` (#8276)

eric-wieser committed 4 years ago

162221fd

docs(order/rel_iso): add module docstring (#8249)

YaelDillies committed 4 years ago

9a801ef6

chore(algebra/quaternion): add `smul_mk` (#8126)

eric-wieser committed 4 years ago

e35d9760

feat(set_theory/cofinality): more infinite pigeonhole principles (#7879)

kim-em committed 4 years ago

610fab7a

feat(logic/embedding): simp lemma for injectivity for embeddings (#7881)

kim-em committed 4 years ago

e6ff367d

docs(data/fintype/basic): add module docstring (#8081)

YaelDillies committed 4 years ago

728eefec

chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325)

eric-wieser committed 4 years ago

4ae97924

feat(measure_theory/conditional_expectation): define condexp_L2, conditional expectation of L2 functions (#8324)

RemyDegenne committed 4 years ago

b577bb2c

feat(ring_theory/ideal): generalize two results from finset to multiset (#8320)

Vierkantor committed 4 years ago

79fbd465

feat(data/matrix/{basic, block}): missing lemmas on conj_transpose (#8303)

eric-wieser committed 4 years ago

a783a47c

feat(algebra/lie/cartan_matrix): define the exceptional Lie algebras (#8299)

ocfnash committed 4 years ago

66055ddf

Older