Documentation Verification Report

Counit

📁 Source: Mathlib/Algebra/MvPolynomial/Counit.lean

Statistics

Metric	Count
Definitions `ACounit`, `counit`, `counitNat`	3
Theorems `ACounit_C`, `ACounit_X`, `ACounit_surjective`, `counitNat_C`, `counitNat_X`, `counitNat_surjective`, `counit_C`, `counit_X`, `counit_surjective`	9
Total	12

MvPolynomial

Definitions

Name	Category	Theorems
`ACounit` 📖	CompOp	3 math math: `ACounit_X`, `ACounit_surjective`, `ACounit_C`
`counit` 📖	CompOp	3 math math: `counit_surjective`, `counit_C`, `counit_X`
`counitNat` 📖	CompOp	3 math math: `counitNat_C`, `counitNat_X`, `counitNat_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ACounit_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `ACounit` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `algebraMap`	—	`aeval_C`
`ACounit_X` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `ACounit` `X`	—	`aeval_X`
`ACounit_surjective` 📖	mathematical	—	`MvPolynomial` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `ACounit`	—	`ACounit_X`
`counitNat_C` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Nat.instCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `counitNat` `C` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ACounit_C`
`counitNat_X` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Nat.instCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `counitNat` `X`	—	`ACounit_X`
`counitNat_surjective` 📖	mathematical	—	`MvPolynomial` `Nat.instCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `counitNat`	—	`ACounit_surjective`
`counit_C` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `counit` `C` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`ACounit_C`
`counit_X` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `counit` `X`	—	`ACounit_X`
`counit_surjective` 📖	mathematical	—	`MvPolynomial` `Int.instCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `counit`	—	`ACounit_surjective`

---

← Back to Index