Commit 2025-01-02 09:59 680465ca

View on Github →

feat: an RCLike field is a real-inner product space of dim at most two (#20321)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

deleted def InnerProductSpace.rclikeToReal

Modified Mathlib/Analysis/RCLike/Lemmas.lean

added theorem RCLike.finrank_le_two

added theorem RCLike.rank_le_two

added theorem RCLike.span_one_I