[Merged by Bors] - refactor: fix LinearMap.coe_mk

[Komyyy]

---

This PR fix LinearMap.coe_mk.

@[simp]
theorem coe_mk {σ : R →+* S} (f : M →+ M₃) (h) :
    ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f

to

@[simp]
theorem coe_mk {σ : R →+* S} (f : M → M₃) (h₁ h₂) :
    ((LinearMap.mk (AddHom.mk f h₁) h₂ : M →ₛₗ[σ] M₃) : M → M₃) = f

[ChrisHughes24]

This seems like it makes the lemma less general. I would suggest maybe changing the statement of LinearMap.coe_mk to the following (changing the coercion from M → M₃ to M →+ M₃.

theorem coe_mk {σ : R →+* S} (f : M →+ M₃) (h) :
    ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M →+ M₃) = f

You could also add AddHom.coe_mk if it's not there already and then the combination of the two lemmas should be able to prove you version of LinearMap.coe_mk.

What do you think @eric-wieser ?

[eric-wieser]

We should have both the version with coe and with coe_fn; I'm a little surprised to hear that Lean3 only has the second of these. Maybe it has both and we forgot to port one of them

[Komyyy]

AddHom.coe_mk is already in the library with a simp attribute, but simp couldn't prove my first version of LinearMap.coe_mk.
I felt something is wrong, and finally found that →+ is actually not AddHom but AddMonoidHom. 🤯
So, the best way is this.

@[simp]
theorem coe_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
    ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f

I also add this.

@[simp]
theorem coe_mk' {σ : R →+* S} (f : AddHom M M₃) (h) :
    ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f

[urkud]

Thanks! 🎉
bors merge

[jcommelin]

bors areyouasleep?

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style