starComp_apply — Mathlib

English

For any a in R, the value of the star-conjugated character equals the conjugate of the original: (starRingEnd) φ (a) = φ(a)¯.

Русский

Для любого a, значение сопряжённой характеристики равно комплексной сопряжённости исходной: (starRingEnd) φ(a) = φ(a)¯.

LaTeX

$$starRingEnd(φ)(a) = φ(a)¯$$

Lean4

theorem starComp_apply (hR : 0 < ringChar R) {φ : AddChar R ℂ} (a : R) : (starRingEnd ℂ) (φ a) = φ⁻¹ a :=
  by
  rw [← starComp_eq_inv hR]
  rfl

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