span_one_I — Mathlib

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]⟩

Похожие утверждения