Theorem rank_submodule_eq_one_iff

Modification history

2024-05-22 08:00
Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
feat(LinearAlgebra/{FiniteDimensional|Dimension/DivisionRing}): relax condition of some results (#12963) …
Added rank_submodule_eq_one_iffView on Github →