Theorems · Theorem · functional analysis
RCLike.rank_le_two
∀ (K : Type u_1) [inst : RCLike K], Module.rank ℝ K ≤ 2
- Defined in
- Mathlib.Analysis.RCLike.Lemmas
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RCLike
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Realstatement and proof · cited by 25,697
- SetLike.coeproof · cited by 8,199
- Submoduleproof · cited by 7,192
- RCLikestatement and proof · cited by 2,829
- Cardinalstatement · cited by 2,598
- Nat.cast_oneproof · cited by 2,501
- Finset.cardproof · cited by 2,327
- Submodule.spanproof · cited by 1,504
- Module.rankstatement and proof · cited by 496
- RCLike.Iproof · cited by 100
- rank_topproof · cited by 9
Cited by1
Results whose statement or proof uses this declaration.
- RCLike.finrank_le_twoproof · cited by 0