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	13 math math: `presburger.funMap_one`, `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.natCast_succ`, `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	9 math math: `funMap_one`, `realize_sum`, `realize_add`, `realize_natCast`, `realize_one`, `realize_zero`, `funMap_zero`, `funMap_add`, `realize_nsmul`
`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.toNatSMul`	—	`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