smulOfNeZero_symm_apply — Mathlib

English

There is a homeomorphism of α onto α given by scalar multiplication by a nonzero element c ∈ G₀.

Русский

Существует гомеоморфизм α в α, заданный умножением на не нулевой элемент c ∈ G₀.

LaTeX

$$$\text{Homeomorph.smulOfNeZero}(c, hc) : \alpha \to_{\text{Homeomorph}} \alpha$$$

Lean4

@[simp]
theorem smulOfNeZero_symm_apply {c : G₀} (hc : c ≠ 0) : ⇑(Homeomorph.smulOfNeZero c hc).symm = (c⁻¹ • · : α → α) :=
  rfl

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