Documentation Verification Report

Defs

📁 Source: SDG/Basic/Defs.lean

Statistics

Metric	Count
Definitions `IsKockLawvere`, `IsKockLawvere_one`, `derivFun`, `instZeroSubtypeMemSubsemigroupD`, `instZeroSubtypeMemSubsemigroup𝔻`, `𝔻`	6
Theorems `D_eq_𝔻_one`, `D_mem_iff`, `isKockLawvere`, `toNontrivial`, `isKockLawvere_one`, `toNontrivial`, `coe_zero`, `instIsKockLawvere_oneOfIsKockLawvere`, `zero_mem_D`, `zero_mem_𝔻`, `𝔻_mem_iff`	11
Total	17

SDG

Definitions

Name	Category	Theorems
`IsKockLawvere` 📖	CompData	—
`IsKockLawvere_one` 📖	CompData	1 math math: `instIsKockLawvere_oneOfIsKockLawvere`
`derivFun` 📖	CompOp	3 math math: `derivFun_unique`, `derivFun_taylor_one`, `derivFun_spec`
`instZeroSubtypeMemSubsemigroupD` 📖	CompOp	—
`instZeroSubtypeMemSubsemigroup𝔻` 📖	CompOp	1 math math: `coe_zero`
`𝔻` 📖	CompOp	8 math math: `coe_pow`, `coe_zero`, `mem_𝔻_of_mem_D_add_mem_D`, `D_eq_𝔻_one`, `𝔻_pow`, `𝔻_mem_iff`, `zero_mem_𝔻`, `𝔻_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`D_eq_𝔻_one` 📖	mathematical	—	`D` `𝔻`	—	—
`D_mem_iff` 📖	mathematical	—	`D`	—	—
`coe_zero` 📖	mathematical	—	`𝔻` `instZeroSubtypeMemSubsemigroup𝔻`	—	—
`instIsKockLawvere_oneOfIsKockLawvere` 📖	mathematical	—	`IsKockLawvere_one`	—	`IsKockLawvere.toNontrivial` `IsKockLawvere.isKockLawvere`
`zero_mem_D` 📖	mathematical	—	`D`	—	—
`zero_mem_𝔻` 📖	mathematical	—	`𝔻`	—	—
`𝔻_mem_iff` 📖	mathematical	—	`𝔻`	—	—

SDG.IsKockLawvere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isKockLawvere` 📖	—	—	—	—	—
`toNontrivial` 📖	—	—	—	—	—

SDG.IsKockLawvere_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isKockLawvere_one` 📖	—	—	—	—	—
`toNontrivial` 📖	—	—	—	—	—

---

← Back to Index