mul — Mathlib

English

The product of two self-adjoint elements is self-adjoint in a commutative semigroup with star.

Русский

Произведение двух самосопряжённых элементов самосопряжено в коммутативном полуграфе со звездой.

LaTeX

$$$\text{IsSelfAdjoint}(x) \rightarrow \text{IsSelfAdjoint}(y) \rightarrow \text{IsSelfAdjoint}(xy)$$$

Lean4

theorem mul {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x * y) := by
  simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]

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