Lift

📁 Source: Mathlib/Algebra/MonoidAlgebra/Lift.lean

Statistics

Metric	Count
Definitions liftNC, liftNCRingHom, liftNC, liftNCRingHom	4
Theorems liftNCRingHom_single, liftNC_mul, liftNC_one, liftNC_single, liftNCRingHom_single, liftNC_mul, liftNC_one, liftNC_single	8
Total	12

AddMonoidAlgebra

Definitions

Name	Category	Theorems
liftNC 📖	CompOp	7 math math: liftNC_mul, Polynomial.eval₂_ofFinsupp, coe_liftNCAlgHom, liftNC_smul, liftNC_single, liftNC_one, lift_def
liftNCRingHom 📖	CompOp	1 math math: liftNCRingHom_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftNCRingHom_single 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike	AddMonoidAlgebra nonAssocSemiring liftNCRingHom single Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	liftNC_single
liftNC_mul 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Multiplicative Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	AddMonoidHom AddMonoidAlgebra AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass instMul	—	MonoidAlgebra.liftNC_mul
liftNC_one 📖	mathematical	—	DFunLike.coe AddMonoidHom AddMonoidAlgebra AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom RingHom Semiring.toNonAssocSemiring AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHom.instFunLike RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Multiplicative zero AddMonoidWithOne.toOne	—	MonoidAlgebra.liftNC_one
liftNC_single 📖	mathematical	—	DFunLike.coe AddMonoidHom AddMonoidAlgebra AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidHom.instFunLike liftNC single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	Finsupp.liftAddHom_apply_single

MonoidAlgebra

Definitions

Name	Category	Theorems
liftNC 📖	CompOp	6 math math: liftNC_mul, coe_liftNCAlgHom, liftNC_single, liftNC_smul, lift_def, liftNC_one
liftNCRingHom 📖	CompOp	1 math math: liftNCRingHom_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftNCRingHom_single 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike	MonoidAlgebra nonAssocSemiring liftNCRingHom single	—	liftNC_single
liftNC_mul 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike	AddMonoidHom MonoidAlgebra AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass instMul	—	RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass sum_single mul_def map_finsuppSum AddMonoidHom.instAddMonoidHomClass liftNC_single Finsupp.sum_mul Finsupp.mul_sum Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_assoc Commute.left_comm
liftNC_one 📖	mathematical	—	DFunLike.coe AddMonoidHom MonoidAlgebra AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom RingHom Semiring.toNonAssocSemiring AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHom.instFunLike RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass one AddMonoidWithOne.toOne	—	RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass liftNC_single map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass mul_one
liftNC_single 📖	mathematical	—	DFunLike.coe AddMonoidHom MonoidAlgebra AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidHom.instFunLike liftNC single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Finsupp.liftAddHom_apply_single

---

← Back to Index