Documentation Verification Report

Basic

📁 Source: Mathlib/ModelTheory/Arithmetic/Presburger/Basic.lean

Statistics

Metric	Count
Definitions `instIsAlgebraicPresburger`, `presburger`, `instAddTerm`, `instNatCastTerm`, `instOneTerm`, `instSMulNatTerm`, `instStructure`, `instZeroTerm`, `sum`, `instDecidableEqPresburgerFunc`, `decEq`, `presburgerFunc`	12
Theorems `funMap_add`, `funMap_one`, `funMap_zero`, `natCast_succ`, `natCast_zero`, `realize_add`, `realize_natCast`, `realize_nsmul`, `realize_one`, `realize_sum`, `realize_zero`, `succ_nsmul`, `zero_nsmul`	13
Total	25

FirstOrder

Definitions

Name	Category	Theorems
`instDecidableEqPresburgerFunc` 📖	CompOp	—
`presburgerFunc` 📖	CompData	—

FirstOrder.Language

Definitions

Name	Category	Theorems
`instIsAlgebraicPresburger` 📖	CompOp	—
`presburger` 📖	CompOp	21 math math: `presburger.mul_not_definable`, `presburger.funMap_one`, `presburger.isSemilinearSet_boundedFormula_realize`, `presburger.zero_nsmul`, `presburger.realize_sum`, `presburger.natCast_zero`, `presburger.realize_add`, `presburger.realize_natCast`, `presburger.realize_one`, `presburger.realize_zero`, `presburger.funMap_zero`, `presburger.funMap_add`, `presburger.realize_nsmul`, `presburger.definable₁_iff_ultimately_periodic`, `IsLinearSet.definable`, `presburger.natCast_succ`, `presburger.term_realize_eq_add_dotProduct`, `presburger.isSemilinearSet_formula_realize_semilinear`, `IsSemilinearSet.definable`, `presburger.definable_iff_isSemilinearSet`, `presburger.succ_nsmul`

FirstOrder.Language.presburger

Definitions

Name	Category	Theorems
`instAddTerm` 📖	CompOp	3 math math: `realize_add`, `natCast_succ`, `succ_nsmul`
`instNatCastTerm` 📖	CompOp	3 math math: `natCast_zero`, `realize_natCast`, `natCast_succ`
`instOneTerm` 📖	CompOp	2 math math: `realize_one`, `natCast_succ`
`instSMulNatTerm` 📖	CompOp	3 math math: `zero_nsmul`, `realize_nsmul`, `succ_nsmul`
`instStructure` 📖	CompOp	17 math math: `mul_not_definable`, `funMap_one`, `isSemilinearSet_boundedFormula_realize`, `realize_sum`, `realize_add`, `realize_natCast`, `realize_one`, `realize_zero`, `funMap_zero`, `funMap_add`, `realize_nsmul`, `definable₁_iff_ultimately_periodic`, `IsLinearSet.definable`, `term_realize_eq_add_dotProduct`, `isSemilinearSet_formula_realize_semilinear`, `IsSemilinearSet.definable`, `definable_iff_isSemilinearSet`
`instZeroTerm` 📖	CompOp	3 math math: `zero_nsmul`, `natCast_zero`, `realize_zero`
`sum` 📖	CompOp	1 math math: `realize_sum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`funMap_add` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `FirstOrder.Language.presburger` `instStructure` `FirstOrder.presburgerFunc.add`	—	—
`funMap_one` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `FirstOrder.Language.presburger` `instStructure` `FirstOrder.presburgerFunc.one`	—	—
`funMap_zero` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `FirstOrder.Language.presburger` `instStructure` `FirstOrder.presburgerFunc.zero`	—	—
`natCast_succ` 📖	mathematical	—	`FirstOrder.Language.Term` `FirstOrder.Language.presburger` `instNatCastTerm` `instAddTerm` `instOneTerm`	—	—
`natCast_zero` 📖	mathematical	—	`FirstOrder.Language.Term` `FirstOrder.Language.presburger` `instNatCastTerm` `instZeroTerm`	—	—
`realize_add` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `FirstOrder.Language.presburger` `instStructure` `FirstOrder.Language.Term` `instAddTerm`	—	—
`realize_natCast` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `FirstOrder.Language.presburger` `instStructure` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `FirstOrder.Language.Term` `instNatCastTerm` `AddMonoidWithOne.toNatCast`	—	`Nat.cast_zero` `Nat.cast_add` `Nat.cast_one`
`realize_nsmul` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `FirstOrder.Language.presburger` `instStructure` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `FirstOrder.Language.Term` `instSMulNatTerm` `AddMonoid.toNSMul`	—	`zero_nsmul` `add_nsmul` `one_smul`
`realize_one` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `FirstOrder.Language.presburger` `instStructure` `FirstOrder.Language.Term` `instOneTerm`	—	—
`realize_sum` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `FirstOrder.Language.presburger` `instStructure` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toOne` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommMonoidWithOne.toAddCommMonoid` `sum` `Finset.sum`	—	`Finset.toList_toFinset` `List.sum_toFinset` `Finset.nodup_toList`
`realize_zero` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `FirstOrder.Language.presburger` `instStructure` `FirstOrder.Language.Term` `instZeroTerm`	—	—
`succ_nsmul` 📖	mathematical	—	`FirstOrder.Language.Term` `FirstOrder.Language.presburger` `instSMulNatTerm` `instAddTerm`	—	—
`zero_nsmul` 📖	mathematical	—	`FirstOrder.Language.Term` `FirstOrder.Language.presburger` `instSMulNatTerm` `instZeroTerm`	—	—

FirstOrder.instDecidableEqPresburgerFunc

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index