toProd_mul — Mathlib

English

For NonemptyInterval α and t, the product (s * t) satisfies (s * t).toProd = s.toProd * t.toProd, i.e., multiplication respects the toProd projection.

Русский

Для непустого интервала s и t произведение удовлетворяет (s * t).toProd = s.toProd · t.toProd, т.е. умножение совместимо с отображением toProd.

LaTeX

$$$(s * t).toProd = s.toProd * t.toProd$$$

Lean4

@[to_additive (attr := simp) toProd_add]
theorem toProd_mul : (s * t).toProd = s.toProd * t.toProd :=
  rfl

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