I_smul_neg_I — Mathlib

English

Multiplication by I is a two-sided inverse to the map a ↦ -i a from skew-adjoint to self-adjoint, i.e., I · (negISMul a) = a.

Русский

Умножение на i является обратным к отображению a ↦ -i a между соответствующими подпространствами: I · (negISMul a) = a.

LaTeX

$$$I\\cdot (\\mathrm{negISMul}\\, a) = a$$$

Lean4

theorem I_smul_neg_I (a : skewAdjoint A) : I • (skewAdjoint.negISMul a : A) = a := by
  simp only [smul_smul, skewAdjoint.negISMul_apply_coe, neg_smul, smul_neg, I_mul_I, one_smul, neg_neg]

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