Commit 2025-12-01 11:03 8e0ed7cb
View on Github →refactor(LinearAlgebra/FiniteDimensional/Defs): move of_fact_finrank_eq_two (#32296)
Move of_fact_finrank_eq_two from Mathlib.Analysis.InnerProductSpace.TwoDim to Mathlib.LinearAlgebra.FiniteDimensional.Defs to avoid a large import in #31891 that was only in order to use that one lemma without needing the rest of Mathlib.Analysis.InnerProductSpace.TwoDim.