Def LinearEquiv.domMulActCongrRight

Modification history

2025-07-15 08:11
Mathlib/Algebra/Module/Equiv/Basic.lean
feat: semilinearize `LinearEquiv.conjRingEquiv` (#27104)
Modified LinearEquiv.domMulActCongrRightView on Github →
2025-05-01 06:42
Mathlib/Algebra/Module/Equiv/Basic.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added LinearEquiv.domMulActCongrRightView on Github →