Theorems · Theorem · combinatorics

IsAddFreimanHom.prodMk

∀ {α : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β₁]
  [inst_2 : AddCommMonoid β₂] {A : Set α} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} {n : ℕ},
  IsAddFreimanHom n A B₁ f₁ → IsAddFreimanHom n A B₂ f₂ → IsAddFreimanHom n A (B₁ ×ˢ B₂) fun x => (f₁ x, f₂ x)

Defined in

Mathlib.Combinatorics.Additive.FreimanHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidAddCommMonoid