instTwoUniqueSums — Mathlib

English

Any FreeAddMonoid κ has the TwoUniqueSums property.

Русский

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

LaTeX

$$$\\text{TwoUniqueSums}(\\mathrm{FreeAddMonoid} \\ k)$$$

Lean4

/-- Any `FreeAddMonoid` has the `TwoUniqueSums` property. -/
instance instTwoUniqueSums {κ : Type*} : TwoUniqueSums (FreeAddMonoid κ) :=
  .of_addHom ⟨_, fun _ _ => List.length_append⟩ (fun _ _ _ _ h h' ↦ List.append_inj h h'.1)

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