Theorems · Theorem · combinatorics

IsAddFreimanHom.comp

∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid γ] {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ},
  IsAddFreimanHom n B C g → IsAddFreimanHom n A B f → IsAddFreimanHom n A C (g ∘ f)

Defined in

Mathlib.Combinatorics.Additive.FreimanHom

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidAddCommMonoid