isSelfAdjoint_algebraMap_iff — Mathlib

English

If the algebra map is injective, then an element r is self-adjoint in R iff its image algebraMap r is self-adjoint in A.

Русский

Если алгебраическая карта инъективна, то r самосопряжён в R тогда и только тогда, когда algebraMap r самосопряжён в A.

LaTeX

$$$(h: \text{Injective } (algebraMap R A)) \Rightarrow (IsSelfAdjoint (algebraMap R A r) \iff IsSelfAdjoint r)$$$

Lean4

theorem isSelfAdjoint_algebraMap_iff {r : R} (h : Function.Injective (algebraMap R A)) :
    IsSelfAdjoint (algebraMap R A r) ↔ IsSelfAdjoint r :=
  ⟨fun hr ↦ h <| algebraMap_star_comm r (A := A) ▸ hr.star_eq, IsSelfAdjoint.algebraMap A⟩

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