mulRight₀_symm_apply — Mathlib

English

For c ≠ 0, the inverse of the right translation by c is the right translation by c⁻¹.

Русский

Для c ≠ 0 обратное преобразование правого умножения на c есть правое умножение на c⁻¹.

LaTeX

$$$((\\mathrm{mulRight}_0(c,hc))^{-1})(x) = x \\cdot c^{-1}$$$

Lean4

@[simp]
theorem mulRight₀_symm_apply (c : α) (hc : c ≠ 0) : ((Homeomorph.mulRight₀ c hc).symm : α → α) = (· * c⁻¹) :=
  rfl

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