mulRight₀ — Mathlib

English

The inverse of the right-translation by a nonzero element is left-translation by its inverse.

Русский

Обратное преобразование правого переноса на ненулевой элемент равно левому переносу на его обратное.

LaTeX

$$((Homeomorph.mulRight₀ c hc).symm) = (λ x, c^{-1} * x)$$

Lean4

/-- Right multiplication by a nonzero element in a `GroupWithZero` with continuous multiplication
is a homeomorphism of the underlying type. -/
protected def mulRight₀ (c : α) (hc : c ≠ 0) : α ≃ₜ α :=
  { Equiv.mulRight₀ c hc with
    continuous_toFun := continuous_mul_right _
    continuous_invFun := continuous_mul_right _ }

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