Def LinearEquiv.conjRingEquiv

Modification history

2025-07-15 08:11

Mathlib/Algebra/Module/Equiv/Basic.lean

feat: semilinearize `LinearEquiv.conjRingEquiv` (#27104)

Modified LinearEquiv.conjRingEquiv View on Github →

2025-05-01 06:42

Mathlib/Algebra/Module/Equiv/Basic.lean

feat: preliminaries for Wedderburn–Artin (#24119)

Modified LinearEquiv.conjRingEquiv View on Github →

2025-01-26 18:07

Mathlib/Algebra/Module/Equiv/Basic.lean

feat(Algebra): `Mul/RingEquiv`s between `center` and `Module.End` (#20721)

Added LinearEquiv.conjRingEquiv View on Github →