conjAe — Mathlib

English

Let K be a complex-like field with a real structure. Conjugation defines an ℝ-algebra automorphism of K.

Русский

Пусть K — поле, подобное комплексному, со структурой над ℝ. Сопряжение задаёт автоморфизм ℝ-алгебры K.

LaTeX

$$$$ conjAe : K \\cong_{\\mathbb{R}} K. $$$$

Lean4

/-- Conjugate as an `ℝ`-algebra equivalence -/
def conjAe : K ≃ₐ[ℝ] K :=
  { conj with
    invFun := conj
    left_inv := conj_conj
    right_inv := conj_conj
    commutes' := conj_ofReal }

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