Def RingEquiv.mopMatrix

Modification history

2025-12-28 17:51

Mathlib/Data/Matrix/Basic.lean

feat(Algebra): stably finite rings (#32262) …

Modified RingEquiv.mopMatrix View on Github →

2024-11-08 13:01

Mathlib/Data/Matrix/Basic.lean

feat(LinearAlgebra/Matrix/ToLin): for R-module M, End(Mⁿ) ≅ Matₙₓₙ(End(M)) (#18752) …

Added RingEquiv.mopMatrix View on Github →