Documentation Verification Report

Applicative

📁 Source: Mathlib/Control/Applicative.lean

Statistics

Metric	Count
Definitions `instApplicativeAddConstOfZeroOfAdd`, `instApplicativeConstOfOneOfMul`	2
Theorems `ext`, `map_seq_map`, `pure_seq_eq_map'`, `seq_mk`, `applicative_comp_id`, `applicative_id_comp`, `instCommApplicative`, `instLawfulApplicativeComp`, `map_pure`, `pure_seq_eq_map`, `seq_assoc`, `seq_pure`, `instCommApplicativeId`, `instLawfulApplicativeAddConst`, `instLawfulApplicativeConst`	15
Total	17

Applicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	—	—	—	`Functor.ext`
`map_seq_map` 📖	—	—	—	—	`seq_map_assoc`
`pure_seq_eq_map'` 📖	—	—	—	—	—

Comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`seq_mk` 📖	mathematical	—	`Functor.Comp` `Functor.Comp.instSeq`	—	—

Functor.Comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`applicative_comp_id` 📖	mathematical	—	`instApplicativeComp`	—	`Applicative.ext` `instLawfulApplicativeComp` `CommApplicative.toLawfulApplicative` `instCommApplicativeId`
`applicative_id_comp` 📖	mathematical	—	`instApplicativeComp`	—	`Applicative.ext` `instLawfulApplicativeComp` `CommApplicative.toLawfulApplicative` `instCommApplicativeId`
`instCommApplicative` 📖	mathematical	—	`CommApplicative` `Functor.Comp` `instApplicativeComp`	—	`instLawfulApplicativeComp` `CommApplicative.toLawfulApplicative` `CommApplicative.commutative_map` `seq_map_assoc`
`instLawfulApplicativeComp` 📖	mathematical	—	`Functor.Comp` `instApplicativeComp`	—	`lawfulFunctor` `pure_seq_eq_map` `map_pure` `seq_pure` `seq_assoc`
`map_pure` 📖	mathematical	—	`Functor.Comp` `functor` `instPure`	—	`ext` `run_pure`
`pure_seq_eq_map` 📖	mathematical	—	`Functor.Comp` `instSeq` `instPure` `functor`	—	`ext` `run_pure`
`seq_assoc` 📖	mathematical	—	`Functor.Comp` `instSeq` `functor`	—	`ext` `seq_map_assoc` `map_seq`
`seq_pure` 📖	mathematical	—	`Functor.Comp` `instSeq` `instPure` `functor`	—	`ext` `run_pure`

(root)

Definitions

Name	Category	Theorems
`instApplicativeAddConstOfZeroOfAdd` 📖	CompOp	1 math math: `instLawfulApplicativeAddConst`
`instApplicativeConstOfOneOfMul` 📖	CompOp	1 math math: `instLawfulApplicativeConst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCommApplicativeId` 📖	mathematical	—	`CommApplicative`	—	—
`instLawfulApplicativeAddConst` 📖	mathematical	—	`Functor.AddConst` `instApplicativeAddConstOfZeroOfAdd` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`Functor.AddConst.lawfulFunctor` `zero_add` `add_zero` `add_assoc`
`instLawfulApplicativeConst` 📖	mathematical	—	`Functor.Const` `instApplicativeConstOfOneOfMul` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul`	—	`Functor.Const.lawfulFunctor` `one_mul` `mul_one` `mul_assoc`

---

← Back to Index