Theorem RCLike.finrank_le_two

Modification history

2025-01-02 09:59
Mathlib/Analysis/RCLike/Lemmas.lean
feat: an `RCLike` field is a real-inner product space of dim at most two (#20321)
Added RCLike.finrank_le_twoView on Github →