constSMul_symm — Mathlib

English

For every c ∈ G, the inverse of the isometry x ↦ c • x is x ↦ c^{-1} • x; i.e., (constSMul c)^{-1} = constSMul(c^{-1}).

Русский

Для каждого c ∈ G обратная векторизованного отображения x ↦ c • x равна отображению x ↦ c^{-1} • x; т.е. (constSMul c)^{-1} = constSMul(c^{-1}).

LaTeX

$$$ (\mathrm{constSMul}\,c)^{-1} = \mathrm{constSMul}\,c^{-1} $$$

Lean4

@[to_additive (attr := simp)]
theorem constSMul_symm (c : G) : (constSMul c : X ≃ᵢ X).symm = constSMul c⁻¹ :=
  ext fun _ => rfl

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