smul_div_smul_comm — Mathlib

English

In a commutative group, the left translate of s divided by the left translate of t equals the left translate by a/b of the quotient s/t: a•s / b•t = (a/b) • (s/t).

Русский

В коммутативной группе левая дробь множества s по a деленная на левую дробь t по b равна левой дроби (a/b) умножение на (s/t).

LaTeX

$$$a \\cdot s / b \\cdot t = (a / b) \\cdot (s / t)$$$

Lean4

@[to_additive]
theorem smul_div_smul_comm (a : α) (s : Set α) (b : α) (t : Set α) : a • s / b • t = (a / b) • (s / t) := by
  simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s, singleton_div_singleton]

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