Theorems · Theorem · combinatorics

IsAddFreimanHom.map_sum_eq_map_sum

∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  IsAddFreimanHom n A B f →
    ∀ ⦃s t : Multiset α⦄,
      (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
        (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
          s.card = n → t.card = n → s.sum = t.sum → (Multiset.map f s).sum = (Multiset.map f t).sum

An additive n-Freiman homomorphism preserves sums of n elements.

Defined in

Mathlib.Combinatorics.Additive.FreimanHom

Cited by

10 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoidAddCommMonoid