[Merged by Bors] - feat(Algebra/Module): Use coercion from SemilinearEquivClass to SemilinearEquiv

[101damnations]

---

Add the coercion from types with a SemilinearEquivClass instance to linear equivs, a la #10758.

[fpvandoorn]

Suggested change

	[EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] : CoeHead F (M ≃ₛₗ[σ] M₂) where
	[EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] : CoeTC F (M ≃ₛₗ[σ] M₂) where

For Equiv and MulEquiv this was done using CoeTC, so I imagine we want that everywhere?

bors d+

[101damnations]

I don't really understand this stuff but judging by this comment it looks like CoeHead is preferred here

[mathlib-bors]

✌️ 101damnations can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[101damnations]

So there's already a coercion from linear equivs to linear maps given by the projection LinearEquiv.toLinearMap, and the following fails if I put it where it makes sense (e.g. after line 202)

example (f : M ≃ₛₗ[σ] M₂) :
    f.toLinearMap = SemilinearMapClass.semilinearMap f := by
  with_reducible rfl

I don't really understand with_reducible, but I guess maybe I should redefine

instance : Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂) :=
  ⟨toLinearMap⟩

on line 153 using SemilinearMapClass.semilinearMap, and deal with the fall out? I guess this potentially means removing a lot of toLinearMaps (and frequently having to replace them with type ascriptions....)

[fpvandoorn]

Thanks for the link. In that case, we should try to fix the existing coercions.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style