Mathlib Map

Theorems · Definition · logic and foundations

IsLinearSet

{M : Type u_1} → [AddCommMonoid M] → Set M → Prop

A set is linear if it is a coset of a finitely generated additive submonoid.

Defined in
Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Cited by
28 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Quot.sound
Assumes
AddCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsSemilinearSet · cited by 44IsSemilinearSetIsLinearSet.isSemilinearSet · cited by 10IsLinearSet.isSemilinearS…IsSemilinearSet.image · cited by 9IsSemilinearSet.imageisLinearSet_iff · cited by 3isLinearSet_iffIsSemilinearSet.union · cited by 3IsSemilinearSet.unionIsSemilinearSet.add · cited by 2IsSemilinearSet.addIsLinearSet.of_fg · cited by 2IsLinearSet.of_fgisSemilinearSet_iff · cited by 1isSemilinearSet_iffisLinearSet_iff_exists_fg_eq_vadd · cited by 1isLinearSet_iff_exists_fg…isLinearSet_iff_exists_fin_addMonoidHom · cited by 1isLinearSet_iff_exists_fi…IsSemilinearSet.definable · cited by 1IsSemilinearSet.definableIsSemilinearSet.empty · cited by 1IsSemilinearSet.emptyIsSemilinearSet.exists_fg_eq_subtypeVal · cited by 1IsSemilinearSet.exists_fg…IsLinearSet.add · cited by 1IsLinearSet.addIsLinearSet.closure · cited by 1IsLinearSet.closureSet · cited by 53352SetAddCommMonoid · cited by 12281AddCommMonoidSetLike.coe · cited by 8199SetLike.coeHVAdd.hVAdd · cited by 1820HVAdd.hVAddSet.Finite · cited by 1814Set.FiniteAddSubmonoid.closure · cited by 224AddSubmonoid.closureIsLinearSetCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by29

Results whose statement or proof uses this declaration.