English
The real rank of the field K is at most 2, due to the span of {1,I} generating the whole space.
Русский
Раnk поля K над Real не превышает 2, так как {1,I} порождают всё пространство.
LaTeX
$$Module.rank Real K ≤ 2$$
Lean4
theorem rank_le_two : Module.rank ℝ K ≤ 2 :=
calc
_ = Module.rank ℝ ↥(Submodule.span ℝ ({ 1, I } : Set K)) := by rw [span_one_I]; simp
_ ≤ #({ 1, I } : Finset K) := by
-- TODO: `simp` doesn't rewrite inside the type argument to `Module.rank`, but `rw` does.
-- We should introduce `Submodule.rank` to fix this.
have := rank_span_finset_le (R := ℝ) (M := K) { 1, I }
rw [Finset.coe_pair] at this
simpa [span_one_I] using this
_ ≤ 2 := mod_cast Finset.card_le_two
