conjugate — Mathlib

English

If x is skew-adjoint, then z * x * star z is skew-adjoint for any z in R.

Русский

Если x — кососопряжённый, то z x z* также кососопряжён для любого z.

LaTeX

$$$ \\forall x \\in \\mathrm{skewAdjoint}(R), \\; \\forall z \\in R, \\; z x \\star z \\in \\mathrm{skewAdjoint}(R). $$$

Lean4

theorem conjugate {x : R} (hx : x ∈ skewAdjoint R) (z : R) : z * x * star z ∈ skewAdjoint R := by
  simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]

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