leanprover-community/mathlib

Pull Requests Commits

Fix usage of `dfinsupp.coe_zero`

Vierkantor committed 3 years ago

67414a22

Lint fix: `to_additive` used in the wrong order, so it wasn't applying nolint

Vierkantor committed 3 years ago

5e9f8c1e

Fix protected `finsupp.coe_add`

Vierkantor committed 3 years ago

178a05be

Fix protected `complex.coe_smul`

Vierkantor committed 3 years ago

2fc790b7

Fix more protected `continuous_map.coe_`

Vierkantor committed 3 years ago

e797e9c4

Do the same but actually correctly this time

Vierkantor committed 3 years ago

97948747

Fix unprotected reference to `continuous_map.coe_`

Vierkantor committed 3 years ago

41bbdd47

Oops, missed a loop

Vierkantor committed 3 years ago

8f0d515f

Make `ereal.coe_` lemmas protected; fix `simp` looping when rewriting to the left with specific lemmas

Vierkantor committed 3 years ago

df2f2cfe

Fix parameter count

Vierkantor committed 3 years ago

4c54cd82

Vierkantor committed 3 years ago

7ecf17db

Fix test: `ennreal.coe_div` is protected

Vierkantor committed 3 years ago

50a8549e

Fix: `complex.coe_smul` should be protected

Vierkantor committed 3 years ago

06c7a487

Vierkantor committed 3 years ago

f4b0ec72

Fix unprotected usage of `ennreal.coe_inv`

Vierkantor committed 3 years ago

9f4e90aa

Fix (`cast_add` has new synonym `coe_add`)

Vierkantor committed 3 years ago

d84d9600

Fix that `measure.coe_add` is protected

Vierkantor committed 3 years ago

cf9fe0a2

Protect `bounded_continuous_function.coe_` lemmas

Vierkantor committed 3 years ago

7f14a4e4

Vierkantor committed 3 years ago

487cb36b

Fix `simp` loop due to `←` + new lemmas

Vierkantor committed 3 years ago

75fdf2b0

Protected `ennreal.coe_` lemmas

Vierkantor committed 3 years ago

381f0e16

Protected `finset.coe_one`

Vierkantor committed 3 years ago

3499acc5

Fix `analysis/inner_product_space/dual.lean` (protected)

Vierkantor committed 3 years ago

73f37f13

Fix `simp` set due to `protected`

Vierkantor committed 3 years ago

4d01bf8d

Make `vector_measure.coe_` lemmas protected

Vierkantor committed 3 years ago

da017070

Fix (protected)

Vierkantor committed 3 years ago

8c5efa16

Fix (changed `simp` set)

Vierkantor committed 3 years ago

3e6d8a51

Fix `simp` loop due to new lemmas

Vierkantor committed 3 years ago

de00f743

Fix more `protected`

Vierkantor committed 3 years ago

f9365c18

Fix (seems to be `simp` order messing things up?)

Vierkantor committed 3 years ago

13c646f2

Older