mul_div_one — Mathlib

English

Let p,r ∈ R and s ∈ S. Then (p / s) * (r / 1) = (p r) / s, expressing multiplication in the localization when the second denominator is 1.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mul_div_one {p r : R} {s : S} : (p /ₒ s) * (r /ₒ 1) = (p * r) /ₒ s := by
  --TODO use coercion r ↦ r /ₒ 1
  simp [oreDiv_mul_char p r s 1 p 1 (by simp)]

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