mul_cancel' — Mathlib

English

Let R be a monoid, S a submonoid with OreSet S, X a MulAction of R on X. Then for all r1, r2 in R and s,t in S, ((r1 * s)/t) * (r2 / s) = (r1 * r2)/t.

Русский

Пусть R — моноид, S — подмоноид, удовлетворяющий Ore-condition, X — действие R на X. Тогда для любых r1,r2 в R и s,t в S выполняется\n((r1 s)/t) * (r2 / s) = (r1 r2)/t.

LaTeX

$$$\\big((r_1 s)/t\\big) \\cdot \\big(r_2 / s\\big) = \\big(r_1 r_2\\big)/t.$$$

Lean4

@[to_additive (attr := simp)]
protected theorem mul_cancel' {r₁ r₂ : R} {s t : S} : ((r₁ * s) /ₒ t) * (r₂ /ₒ s) = (r₁ * r₂) /ₒ t := by
  simp [oreDiv_mul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

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