leanprover-community/mathlib

Pull Requests Commits

`protected` in `linear_map.coe_` and `special_linear_group.coe_`

Vierkantor committed 3 years ago

7a818a80

Fix missing names (apparently there's now a name conflict with `power_series`?)

Vierkantor committed 3 years ago

2d5ab30e

Even more `protected`

Vierkantor committed 3 years ago

e5a16184

More `protected`

Vierkantor committed 3 years ago

c419c407

Make `lucas_lehmer.X.coe_mul` `protected`

Vierkantor committed 3 years ago

5c89ca01

`coe_ring_hom` instance for `power_series` (+ protected)

Vierkantor committed 3 years ago

d2eac817

Make `add_monoid_hom.coe_mul` protected

Vierkantor committed 3 years ago

463f570e

Make `continuous_map.coe_` lemmas protected

Vierkantor committed 3 years ago

f753c8db

More `protected` in `finsupp` and `dfinsupp`

Vierkantor committed 3 years ago

d223d978

More `protected`

Vierkantor committed 3 years ago

f6aafc22

Protect `coe_` lemmas for `uniform_space.completion`

Vierkantor committed 3 years ago

13aa2b3b

Fix `mul_comm` firing at a different moment while `simp`ing

Vierkantor committed 3 years ago

8267447a

Fix `data/zmod/basic` (`simp` doesn't pick up on `coe_zero` but does like `int.cast_zero`)

Vierkantor committed 3 years ago

ba387bd1

Protected `dfinsupp.coe_` lemmas

Vierkantor committed 3 years ago

46bd1d8f

Make some `finsupp.coe_` lemmas `protected`

Vierkantor committed 3 years ago

644f728a

`coe_ring_hom` for `nnrat`

Vierkantor committed 3 years ago

4b56aa5e

`coe_hom` instance for submodule → module coercion

Vierkantor committed 3 years ago

57bd2ae7

Add classes for coercions that are linear/semilinear maps

Vierkantor committed 3 years ago

3f0791ac

Add special-case `coe_one_hom` instance for `nat`

Vierkantor committed 3 years ago

93bb4fbd

`coe_ring_hom` should also weaken to `coe_monoid_with_zero_hom`

Vierkantor committed 3 years ago

441b9aca

More `cast` lemmas that don't need `@[simp]` anymore

Vierkantor committed 3 years ago

5decc005

Re-add `@[norm_cast]` attribute (not completely sure why it's needed)

Vierkantor committed 3 years ago

486a043c

Remove `simp`/`norm_cast` attributes from `nat` and `int` cast

Vierkantor committed 3 years ago

15fdaf38

`coe_bit0` and `coe_bit1` lemmas

Vierkantor committed 3 years ago

c765b162

Fix this simp call looping between `coe_add` and `←nat.cast_add`

Vierkantor committed 3 years ago

c09856df

`coe_ring_hom` instance for `enat`

Vierkantor committed 3 years ago

743d3841

Add `norm_cast` attributes

Vierkantor committed 3 years ago

2397ef52

Use the coe classes for sub(semi)rings

Vierkantor committed 3 years ago

28431ce4

`coe_ring_hom` for `ℚ`

Vierkantor committed 3 years ago

2959da60

`coe_pow` lemmas

Vierkantor committed 3 years ago

d6d185d3

Newer Older