addHom_ext — Mathlib

English

If two additive monoid homomorphisms f,g: Multiset α → β agree on all singleton multisets, then f = g.

Русский

Если два гомоморфизмаAddMonoidHom f,g: Multiset α → β совпадают на всех одиночных мультимножествах, то они равны.

LaTeX

$$$\forall x, f\{x\} = g\{x\} \implies f = g.$$$

Lean4

@[ext]
theorem addHom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f { x } = g { x }) : f = g :=
  by
  ext s
  induction s using Multiset.induction_on with
  | empty => simp only [_root_.map_zero]
  | cons a s ih => simp only [← singleton_add, _root_.map_add, ih, h]

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