smul_div_one — Mathlib

English

Let p ∈ R, r ∈ X, s ∈ S. Then (p / s) • (r / 1) = (p • r) / s, describing compatibility of smul with localization when the divisor is 1.

Русский

Пусть p ∈ R, r ∈ X, s ∈ S. Тогда (p / s) • (r / 1) = (p • r) / s, что выражает совместимость скалятора с локализацией при делителе 1.

LaTeX

$$$\\big(p / s\\big) \\cdot \\big(r / 1\\big) = \\big(p \\cdot r\\big)/s.$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_div_one {p : R} {r : X} {s : S} : (p /ₒ s) • (r /ₒ 1) = (p • r) /ₒ s := by
  simp [oreDiv_smul_char p r s 1 p 1 (by simp)]

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