smul_top — Mathlib

English

Let R act on ENNReal with suitable properties. Then c • ∞ = 0 if c = 0, and c • ∞ = ∞ if c ≠ 0.

Русский

Пусть R действует на ENNReal; тогда c • ∞ = 0 при c = 0, иначе c • ∞ = ∞.

LaTeX

$$$ c \cdot \infty = \begin{cases}0, & c = 0 \\ \infty, & c \neq 0\end{cases}.$$$

Lean4

theorem smul_top {R} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [NoZeroSMulDivisors R ℝ≥0∞]
    [DecidableEq R] (c : R) : c • ∞ = if c = 0 then 0 else ∞ :=
  by
  rw [← smul_one_mul, mul_top']
  simp_rw [smul_eq_zero, or_iff_left one_ne_zero]

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