Theorem Subalgebra.bot_eq_top_iff_finrank_eq_one

Modification history

2024-05-24 11:39

Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot (#12849) …

Modified Subalgebra.bot_eq_top_iff_finrank_eq_one View on Github →

2023-04-25 11:42

Mathlib/LinearAlgebra/FiniteDimensional.lean

feat: port LinearAlgebra.FiniteDimensional (#3466)

Added Subalgebra.bot_eq_top_iff_finrank_eq_one View on Github →