Def AddEquiv.linearEquiv

Modification history

2026-08-10 23:43
Mathlib/Algebra/Module/TransferInstance.lean
feat: generalize transfer instance type class assumptions (#42291) …
Modified AddEquiv.linearEquivView on Github →
2026-02-23 20:15
Mathlib/Algebra/Module/TransferInstance.lean
feat(RingTheory/IsTensorProduct): heterogeneous associativity (#35557) …
Added AddEquiv.linearEquivView on Github →