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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike ACounit RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C algebraMap	—	aeval_C
ACounit_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike ACounit X	—	aeval_X
ACounit_surjective 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike ACounit	—	ACounit_X
counitNat_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Nat.instCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike counitNat C AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ACounit_C
counitNat_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Nat.instCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike counitNat X	—	ACounit_X
counitNat_surjective 📖	mathematical	—	MvPolynomial Nat.instCommSemiring DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike counitNat	—	ACounit_surjective
counit_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring CommRing.toCommSemiring RingHom.instFunLike counit C AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	ACounit_C
counit_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring CommRing.toCommSemiring RingHom.instFunLike counit X	—	ACounit_X
counit_surjective 📖	mathematical	—	MvPolynomial Int.instCommSemiring DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring CommRing.toCommSemiring RingHom.instFunLike counit	—	ACounit_surjective

---

← Back to Index