coe_mulRight₀ — Mathlib

English

Let α be a topological space with a GroupWithZero structure and continuous multiplication. For any nonzero c, the map x ↦ x c is a homeomorphism; its underlying function is right multiplication by c.

Русский

Пусть α — топологическое пространство, обладающее структурой группы с нулём и непрерывным умножением. Для любого ненулевого c отображение x ↦ x c является гомеоморфизмом; его базовая функция равна правому умножению на c.

LaTeX

$$$\\forall x, ((\\mathrm{mulRight}_0(c,hc))(x) = x \\cdot c)$$$

Lean4

@[simp]
theorem coe_mulRight₀ (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulRight₀ c hc) = (· * c) :=
  rfl

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