English
In a DivInvMonoid β with a scalar action of α that is compatible with division, the action commutes with division: r • x / y = r • (x / y) for all r in α and x, y in β.
Русский
Пусть β — делоподобная монодиальная структура, на β действует α скалярами совместно с операцией деления. Тогда r • x / y = r • (x / y) для всех r ∈ α и x, y ∈ β.
LaTeX
$$$\\\\forall r \\\\in \\\\alpha, \\\\forall x, y \\\\in \\\\beta, \\\\ r \\\\cdot x / y = r \\\\cdot (x / y).$$$
Lean4
/-- Note that the `IsScalarTower α β β` typeclass argument is usually satisfied by `Algebra α β`. -/
@[to_additive]
theorem smul_div_assoc [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) : r • x / y = r • (x / y) :=
by simp [div_eq_mul_inv, smul_mul_assoc]
