conjugate' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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