liftAux_neg_I — Mathlib

English

For a real algebra A with a complex structure, the lift sending the scalar -i to the conjugation automorphism equals conjAe; i.e., the liftAux at -i coincides with the conjugation automorphism.

Русский

Для вещественной алгебры A с комплексной структурой существует равенство подъёма, отправляющего -i в автоморфизм сопряжения, и conjAe: liftAux(-i) = conjAe.

LaTeX

$$$\\mathrm{liftAux}(-i) = \\mathrm{conjAe}$$$

Lean4

@[simp]
theorem liftAux_neg_I : liftAux (-I) ((neg_mul_neg _ _).trans I_mul_I) = conjAe :=
  algHom_ext <| (liftAux_apply_I _ _).trans conj_I.symm

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