Theorem RCLike.span_one_I

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.span_one_IView on Github →