oreDiv_one_smul — Mathlib

English

For r ∈ R and x ∈ X[S⁻¹], the action by oreDiv(r,1) coincides with the standard action: oreDiv(r,1) smul x = r smul x.

Русский

Действие oreDiv(r,1) на x совпадает с обычным действием: oreDiv(r,1) smul x = r smul x.

LaTeX

$$$(\\text{oreDiv}(r,1)) \\cdot x = r \\cdot x.$$$

Lean4

@[to_additive (attr := simp)]
theorem oreDiv_one_smul (r : M) (x : X[S⁻¹]) : (r /ₒ (1 : S)) • x = r • x :=
  by
  cases x
  rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]

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