Theorem Module.End.injective_of_surjective

Modification history

2025-12-28 17:51
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean
feat(Algebra): stably finite rings (#32262) …
Added Module.End.injective_of_surjectiveView on Github →