out_mul — Mathlib

English

Let α be a CancelCommMonoidWithZero and a NormalizationMonoid. The representative map respects multiplication: out(a b) = out(a) out(b) for all a,b in Associates α.

Русский

Пусть α имеет CancelCommMonoidWithZero и NormalizationMonoid. Репрезентативное отображение сохраняет умножение: out(a b) = out(a) out(b) для всех a,b ∈ Associates α.

LaTeX

$$$$ \\operatorname{out}(a b) = \\operatorname{out}(a)\\operatorname{out}(b) $$$$

Lean4

theorem out_mul (a b : Associates α) : (a * b).out = a.out * b.out :=
  Quotient.inductionOn₂ a b fun _ _ => by simp only [Associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize.map_mul]

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