adjoin_I — Mathlib

English

The real-subalgebra generated by the imaginary unit I is all of ℂ, i.e., adjoinℝ({I}) = ⊤.

Русский

Реальная подалгебра, порожденная мнимой единицей I, равна всему ℂ, то есть adjoinℝ({I}) = ⊤.

LaTeX

$$$ \operatorname{adjoin}_{\\mathbb{R}}(\{ i \}) = \top. $$$

Lean4

@[simp]
theorem adjoin_I : Algebra.adjoin ℝ { I } = ⊤ :=
  by
  refine top_unique fun x hx => ?_; clear hx
  rw [← x.re_add_im, ← smul_eq_mul, ← Complex.coe_algebraMap]
  exact add_mem (algebraMap_mem _ _) (Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _)

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