Theorems · Theorem · combinatorics

IsMulFreimanHom.mono

∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {m n : ℕ}, m ≤ n → IsMulFreimanHom n A B f → IsMulFreimanHom m A B f

Defined in

Mathlib.Combinatorics.Additive.FreimanHom

Cited by

1 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidCancelCommMonoid