smul_oreDiv_one — Mathlib

English

For any r ∈ R and x ∈ X, r • (x / 1) equals (r • x) / 1, i.e., localization commutes with smul by R.

Русский

Для любого r ∈ R и x ∈ X выполняется r • (x / 1) = (r • x) / 1, то есть локализация сохраняет скалярное умножение.

LaTeX

$$$\\text{smul\_oreDiv\_one}(r,x) : r \\cdot (x/1) = (r \\cdot x)/1$$$

Lean4

@[to_additive]
theorem smul_oreDiv_one (r : R) (x : X) : r • (x /ₒ (1 : S)) = (r • x) /ₒ (1 : S) := by
  rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, one_smul]

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