instTwoUniqueProds — Mathlib

English

Any FreeMonoid κ has the TwoUniqueProds property.

Русский

У любого свободного моноида κ имеется свойство TwoUniqueProds.

LaTeX

$$$\\text{TwoUniqueProds}(\\mathrm{FreeMonoid} \\ k)$$$

Lean4

/-- Any `FreeMonoid` has the `TwoUniqueProds` property. -/
instance instTwoUniqueProds {κ : Type*} : TwoUniqueProds (FreeMonoid κ) :=
  .of_mulHom ⟨Multiplicative.ofAdd ∘ List.length, fun _ _ ↦ congr_arg _ List.length_append⟩
    (fun _ _ _ _ h h' ↦ List.append_inj h <| Equiv.injective Multiplicative.ofAdd h'.1)

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