English
The span over the reals of {1, I} inside the complex-like field K equals the whole space.
Русский
Образ подпространства над Real порожденного {1, I} равен всему пространству.
LaTeX
$$Submodule.span Real (M := K) { 1, I } = ⊤$$
Lean4
theorem span_one_I : Submodule.span ℝ (M := K) { 1, I } = ⊤ :=
by
suffices ∀ x : K, ∃ a b : ℝ, a • 1 + b • I = x by simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]
exact fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩