Theorem FiniteDimensional.of_fact_finrank_eq_two

Modification history

2025-12-01 11:03

Mathlib/Analysis/InnerProductSpace/TwoDim.lean

refactor(LinearAlgebra/FiniteDimensional/Defs): move `of_fact_finrank_eq_two` (#32296) …

Modified FiniteDimensional.of_fact_finrank_eq_two View on Github →

2024-02-02 21:55

Mathlib/Analysis/InnerProductSpace/TwoDim.lean

chore(FiniteDimensional): rename lemmas (#10188) …

Added FiniteDimensional.of_fact_finrank_eq_two View on Github →