leanprover-community/mathlib3

Pull Requests Commits

use the new lemma

eric-wieser committed 2 years ago

8205ecbe

another Sort version

eric-wieser committed 2 years ago

2eaedc13

eric-wieser committed 2 years ago

8e36048b

hrmacbeth committed 2 years ago

a4e50387

weaken to Sort where possible

hrmacbeth committed 2 years ago

9bef5c72

Update src/measure_theory/function/strongly_measurable/ae_sequence.lean

AlexKontorovich committed 2 years ago

Verified 0e772d4a

Update src/measure_theory/function/strongly_measurable/ae_sequence.lean

AlexKontorovich committed 2 years ago

Verified 8cf7f021

generalize to Sort

eric-wieser committed 2 years ago

843984d5

Update src/measure_theory/function/strongly_measurable/ae_sequence.lean

AlexKontorovich committed 2 years ago

Verified 95178fd8

Update src/measure_theory/function/strongly_measurable/ae_sequence.lean

AlexKontorovich committed 2 years ago

Verified a95ee5c9

Update src/measure_theory/function/strongly_measurable/ae_sequence.lean

AlexKontorovich committed 2 years ago

Verified 89918379

Update src/measure_theory/function/strongly_measurable/basic.lean

AlexKontorovich committed 2 years ago

Verified 8007fea1

Update src/measure_theory/function/strongly_measurable/basic.lean

AlexKontorovich committed 2 years ago

Verified 8a555256

Update src/measure_theory/function/strongly_measurable/ae_sequence.lean

AlexKontorovich committed 2 years ago

Verified f4104e1d

Update src/measure_theory/function/strongly_measurable/ae_sequence.lean

AlexKontorovich committed 2 years ago

Verified 0222b11a

Update src/measure_theory/function/strongly_measurable/supr.lean

AlexKontorovich committed 2 years ago

Verified 57df3c74

Update src/measure_theory/function/strongly_measurable/supr.lean

AlexKontorovich committed 2 years ago

Verified 0d547655

Update src/measure_theory/function/strongly_measurable/supr.lean

AlexKontorovich committed 2 years ago

Verified e5bb1fb4

Update src/measure_theory/function/strongly_measurable/supr.lean

AlexKontorovich committed 2 years ago

Verified 03834466

AlexKontorovich committed 2 years ago

7709ea25

AlexKontorovich committed 2 years ago

8734451e

nonempty take 3

AlexKontorovich committed 2 years ago

3fc5302b

AlexKontorovich committed 2 years ago

883e2867

AlexKontorovich committed 2 years ago

3f8b20a7

AlexKontorovich committed 2 years ago

b864ce91

AlexKontorovich committed 2 years ago

80350dc8

AlexKontorovich committed 2 years ago

fb6582a9

AlexKontorovich committed 2 years ago

d4154172

feat(data/list/of_fn): two lemmas about tuple concatenation (#18192)

eric-wieser committed 2 years ago

fd838fdf

feat(ring_theory/power_basis): matrix of multiplication by generator (#18177)

alreadydone committed 2 years ago

d1d69e99

Older