prodAssoc — Mathlib

English

The associativity of products yields a multiplicative equivalence between ((M × N) × P) and (M × (N × P)).

Русский

Сопоставление тройного произведения дает мультипликативное эквивалентность между ((M × N) × P) и (M × (N × P)).

LaTeX

$$$((M \\times N) \\times P) \\cong_* (M \\times (N \\times P))$$$

Lean4

/-- The equivalence between `(M × N) × P` and `M × (N × P)` is multiplicative. -/
@[to_additive prodAssoc /-- The equivalence between `(M × N) × P` and `M × (N × P)` is additive. -/
    ]
def prodAssoc : (M × N) × P ≃* M × (N × P) :=
  { Equiv.prodAssoc M N P with map_mul' := fun ⟨_, _⟩ ⟨_, _⟩ => rfl }

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