smulOfNeZero — Mathlib

English

For c ≠ 0, interior(c · s) = c · interior(s).

Русский

Для c ≠ 0 выполняется interior(c · s) = c · interior(s).

LaTeX

$$$\operatorname{int}(c \cdot s) = c \cdot \operatorname{int}(s)$$$

Lean4

/-- Scalar multiplication by a non-zero element of a group with zero acting on `α` is a
homeomorphism from `α` onto itself. -/
@[simps! -fullyApplied apply]
protected def smulOfNeZero (c : G₀) (hc : c ≠ 0) : α ≃ₜ α :=
  Homeomorph.smul (Units.mk0 c hc)

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