Theorem Module.finrank_top_le_finrank_of_isScalarTower_of_free

Modification history

2025-05-19 06:33
Mathlib/LinearAlgebra/Dimension/Free.lean
feat: miscellaneous lemmas about transcendence bases (#24344)
Added Module.finrank_top_le_finrank_of_isScalarTower_of_freeView on Github →