Theorem finrank_le_of_span_eq_top

Modification history

2024-10-14 12:17
Mathlib/LinearAlgebra/Dimension/Constructions.lean
feat: add `RingTheory.Trace.Quotient`: relations between trace maps and quotients (#14798) …
Added finrank_le_of_span_eq_topView on Github →