coe_prodAssoc — Mathlib

English

The underlying function of the prodAssoc equivalence is the standard associativity isomorphism on triple products.

Русский

Функционная часть эквивалентности prodAssoc совпадает с обычным изоморфизмом ассоциативности тройного произведения.

LaTeX

$$$\\mathrm{coe}(\\mathrm{prodAssoc}) = \\mathrm{Equiv.prodAssoc}$$$

Lean4

@[to_additive (attr := simp) coe_prodAssoc]
theorem coe_prodAssoc : ⇑(prodAssoc : (M × N) × P ≃* M × (N × P)) = Equiv.prodAssoc M N P :=
  rfl

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