Theorems · Theorem · logic and foundations

isSemilinearSet_setOfPred_eq

∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [AddMonoid.FG M] {F : Type u_5}
  {G : Type u_6} [inst_3 : FunLike F M N] [AddMonoidHomClass F M N] [inst_5 : FunLike G M N] [AddMonoidHomClass G M N]
  (a b : N) (f : F) (g : G), IsSemilinearSet {x | a + f x = b + g x}

The set of solutions to a linear equation a + f x = b + g y in a finitely generated monoid is semilinear.

Defined in

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidAddMonoid.FGFunLikeAddMonoidHomClassFunLikeAddMonoidHomClass