Theorem AffineMap.finrank_eq

Modification history

2026-03-25 14:50
Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
feat(LinearAlgebra): dimension of `P →ᵃ[R] W` (#36006)
Added AffineMap.finrank_eqView on Github →