conjAe — Mathlib

English

There exists an ℝ-algebra isomorphism conjAe: ℂ ≃ₐ[ℝ] ℂ given by complex conjugation.

Русский

Существуют ℝ-алгебра-изоморфизм conjAe: ℂ ≃ₐ[ℝ] ℂ, заданный комплексным сопряжением.

LaTeX

$$$ conjAe : \mathbb{C} \cong_{\mathbb{R}} \mathbb{C} \\text{is an } \mathbb{R}\text{-algebra isomorphism (conjugation).} $$$

Lean4

/-- `ℝ`-algebra isomorphism version of the complex conjugation function from `ℂ` to `ℂ` -/
def conjAe : ℂ ≃ₐ[ℝ] ℂ :=
  { conj with
    invFun := conj
    left_inv := star_star
    right_inv := star_star
    commutes' := conj_ofReal }

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