algebraMap — Mathlib

English

If r is self-adjoint in R, then its image under the algebra map is self-adjoint in A.

Русский

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

LaTeX

$$IsSelfAdjoint r → IsSelfAdjoint (algebraMap R A r)$$

Lean4

protected theorem algebraMap {r : R} (hr : IsSelfAdjoint r) : IsSelfAdjoint (algebraMap R A r) := by
  simpa using congr(algebraMap R A $(hr.star_eq))

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