Theorems · Theorem · combinatorics

IsMulFreimanIso.map_prod_eq_map_prod

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

An n-Freiman homomorphism preserves products of n elements.

Defined in

Mathlib.Combinatorics.Additive.FreimanHom

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoid