GroupRingAction

📁 Source: Mathlib/Algebra/Polynomial/GroupRingAction.lean

Statistics

Metric	Count
Definitions polynomial, instMulSemiringAction, prodXSubSMul	3
Theorems coe_polynomial, eval_smul', smul_X, smul_eq_map, smul_eval, smul_eval_smul, coeff, eval, monic, smul	10
Total	13

MulSemiringActionHom

Definitions

Name	Category	Theorems
polynomial 📖	CompOp	1 math math: coe_polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_polynomial 📖	mathematical	—	DFunLike.coe MulSemiringActionHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.instMulSemiringAction instFunLike polynomial Polynomial.map RingHomClass.toRingHom Semiring.toNonAssocSemiring MulSemiringActionSemiHomClass.toRingHomClass MonoidHom MonoidHom.instFunLike MulSemiringAction.toDistribMulAction instMulSemiringActionSemiHomClassCoeMonoidHom	—	—

Polynomial

Definitions

Name	Category	Theorems
instMulSemiringAction 📖	CompOp	1 math math: MulSemiringActionHom.coe_polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval_smul' 📖	mathematical	—	eval CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Polynomial instZero smulZeroClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_eval_smul smul_inv_smul
smul_X 📖	mathematical	—	Polynomial SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction X	—	map_X smul_eq_map
smul_eq_map 📖	mathematical	—	Polynomial SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction map MulSemiringAction.toRingHom	—	ext coeff_smul coeff_map
smul_eval 📖	mathematical	—	eval CommSemiring.toSemiring Polynomial SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction AddZero.toZero AddZeroClass.toAddZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_eval_smul smul_inv_smul
smul_eval_smul 📖	mathematical	—	eval CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Polynomial instZero smulZeroClass	—	induction_on smul_C eval_C smul_add eval_add smul_mul' smul_pow' smul_X eval_mul eval_X_pow

(root)

Definitions

Name	Category	Theorems
prodXSubSMul 📖	CompOp	4 math math: prodXSubSMul.smul, prodXSubSMul.monic, prodXSubSMul.coeff, prodXSubSMul.eval

prodXSubSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Ring.toSemiring Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring prodXSubSMul	—	Polynomial.coeff_smul smul
eval 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring prodXSubSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	map_prod MonoidHom.instMonoidHomClass Finset.prod_eq_zero Finset.mem_univ MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_C sub_self
monic 📖	mathematical	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring prodXSubSMul	—	Polynomial.monic_prod_of_monic Polynomial.monic_X_sub_C
smul 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul Polynomial.instZero Polynomial.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Ring.toSemiring prodXSubSMul	—	Finset.smul_prod' Fintype.prod_bijective MulAction.left_quotientAction MulAction.bijective MulAction.ofQuotientStabilizer_smul smul_sub Polynomial.smul_X Polynomial.smul_C

---

← Back to Index