smul_cancel' — Mathlib

English

Let R be a monoid, S a submonoid satisfying the Ore condition, X a left R-set. Then for all r1 in R, r2 in X, s,t in S, one has ((r1 s)/t) • (r2 / s) = (r1 • r2) / t.

Русский

Пусть R — моноид, S — подмоноид, удовлетворяющий условию Эн-Ора, X — левое множество-R. Тогда для любых r1 в R, r2 в X и любых 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 \\cdot r_2\\big)/t.$$$

Lean4

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

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