Theorem Module.Finite.of_isComplemented_codomain

Modification history

2025-09-04 11:48

Mathlib/RingTheory/SimpleModule/Basic.lean

feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End` (#24015)

Added Module.Finite.of_isComplemented_codomain View on Github →