Basic

📁 Source: Mathlib/Algebra/Polynomial/Module/Basic.lean

Statistics

Metric	Count
Definitions `PolynomialModule`, `comp`, `equivPolynomial`, `equivPolynomialSelf`, `eval`, `instModule`, `lsingle`, `map`, `polynomialModule`, `single`, `instAddCommGroupPolynomialModule`, `instCoeFunPolynomialModuleForallNat`, `instFunLikePolynomialModuleNat`, `instInhabitedPolynomialModule`	14
Theorems `add_apply`, `aeval_equivPolynomial`, `comp_apply`, `comp_eval`, `comp_single`, `comp_smul`, `equivPolynomialSelf_apply_eq`, `equivPolynomial_single`, `eval_apply`, `eval_lsingle`, `eval_map`, `eval_map'`, `eval_single`, `eval_smul`, `hom_ext`, `hom_ext_iff`, `induction_linear`, `instIsScalarTower`, `isScalarTower'`, `lsingle_apply`, `map_lsingle`, `map_single`, `map_smul`, `monomial_smul_apply`, `monomial_smul_lsingle`, `monomial_smul_single`, `single_apply`, `single_smul`, `smul_apply`, `smul_def`, `smul_single_apply`, `zero_apply`	32
Total	46

PolynomialModule

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	5 math math: `taylorWithin_succ`, `comp_single`, `comp_smul`, `comp_apply`, `comp_eval`
`equivPolynomial` 📖	CompOp	3 math math: `aeval_equivPolynomial`, `equivPolynomial_single`, `equivPolynomialSelf_apply_eq`
`equivPolynomialSelf` 📖	CompOp	3 math math: `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `equivPolynomialSelf_apply_eq`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`
`eval` 📖	CompOp	12 math math: `Derivation.apply_eval_eq`, `eval_map`, `aeval_equivPolynomial`, `comp_apply`, `eval_lsingle`, `eval_apply`, `eval_smul`, `comp_eval`, `Derivation.apply_aeval_eq'`, `eval_map'`, `eval_single`, `Derivation.apply_aeval_eq`
`instModule` 📖	CompOp	32 math math: `Derivation.apply_eval_eq`, `taylorWithin_succ`, `comp_single`, `map_lsingle`, `eval_map`, `map_smul`, `comp_smul`, `aeval_equivPolynomial`, `Derivation.mapCoeffs_X`, `Derivation.mapCoeffs_C`, `single_smul`, `Derivation.mapCoeffs_monomial`, `isScalarTower'`, `comp_apply`, `eval_lsingle`, `equivPolynomial_single`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `equivPolynomialSelf_apply_eq`, `instIsScalarTower`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `lsingle_apply`, `eval_apply`, `eval_smul`, `comp_eval`, `Derivation.mapCoeffs_apply`, `Derivation.apply_aeval_eq'`, `monomial_smul_lsingle`, `eval_map'`, `hom_ext_iff`, `map_single`, `eval_single`, `Derivation.apply_aeval_eq`
`lsingle` 📖	CompOp	6 math math: `map_lsingle`, `comp_apply`, `eval_lsingle`, `lsingle_apply`, `monomial_smul_lsingle`, `hom_ext_iff`
`map` 📖	CompOp	8 math math: `map_lsingle`, `eval_map`, `map_smul`, `aeval_equivPolynomial`, `comp_apply`, `Derivation.apply_aeval_eq'`, `eval_map'`, `map_single`
`polynomialModule` 📖	CompOp	28 math math: `Ideal.Filtration.submodule_closure_single`, `Derivation.apply_eval_eq`, `Ideal.Filtration.submodule_eq_span_le_iff_stable_ge`, `comp_single`, `smul_def`, `map_smul`, `comp_smul`, `Derivation.mapCoeffs_X`, `Ideal.Filtration.mem_submodule`, `monomial_smul_single`, `Derivation.mapCoeffs_C`, `Derivation.mapCoeffs_monomial`, `isScalarTower'`, `Ideal.Filtration.inf_submodule`, `comp_apply`, `Ideal.Filtration.submodule_span_single`, `smul_apply`, `smul_single_apply`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `equivPolynomialSelf_apply_eq`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `eval_smul`, `Derivation.mapCoeffs_apply`, `monomial_smul_apply`, `Derivation.apply_aeval_eq'`, `monomial_smul_lsingle`, `Ideal.Filtration.submodule_fg_iff_stable`, `Derivation.apply_aeval_eq`
`single` 📖	CompOp	14 math math: `Ideal.Filtration.submodule_closure_single`, `Ideal.Filtration.submodule_eq_span_le_iff_stable_ge`, `taylorWithin_succ`, `comp_single`, `monomial_smul_single`, `Derivation.mapCoeffs_C`, `single_smul`, `Derivation.mapCoeffs_monomial`, `single_apply`, `Ideal.Filtration.submodule_span_single`, `equivPolynomial_single`, `smul_single_apply`, `map_single`, `eval_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instFunLike` `PolynomialModule` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule`	—	`Finsupp.add_apply`
`aeval_equivPolynomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PolynomialModule` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.toModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `instModule` `Polynomial.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `equivPolynomial` `LinearMap` `Semiring.toModule` `LinearMap.instFunLike` `eval` `map` `Algebra.linearMap`	—	`induction_linear` `RingHomInvPair.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `equivPolynomial_single` `Polynomial.aeval_monomial` `mul_comm` `map_single` `Algebra.linearMap_apply` `eval_single` `smul_eq_mul`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `comp` `Polynomial` `Polynomial.commRing` `polynomialModule` `eval` `map` `lsingle`	—	—
`comp_eval` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `eval` `comp` `Polynomial.eval`	—	`RingHomCompTriple.ids` `LinearMap.comp_apply` `induction_linear` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `comp_single` `eval_single` `eval_smul` `Polynomial.eval_pow` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.cast_pos`
`comp_single` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `comp` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `single` `Polynomial` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `polynomialModule` `Monoid.toNatPow`	—	`comp_apply` `map_single` `eval_single`
`comp_smul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `comp` `Polynomial` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `polynomialModule` `Polynomial.comp`	—	`comp_apply` `map_smul` `isScalarTower'` `IsScalarTower.left` `eval_smul` `Polynomial.comp.eq_1` `Polynomial.eval_map`
`equivPolynomialSelf_apply_eq` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PolynomialModule` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `polynomialModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `equivPolynomialSelf` `Algebra.toModule` `Algebra.id` `instModule` `Polynomial.module` `equivPolynomial`	—	`RingHomInvPair.ids`
`equivPolynomial_single` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PolynomialModule` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.toModule` `Polynomial` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `instModule` `Polynomial.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `equivPolynomial` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `single` `LinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.monomial`	—	`RingHomInvPair.ids`
`eval_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `eval` `Finsupp.sum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Monoid.toNatPow`	—	—
`eval_lsingle` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `eval` `lsingle` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Monoid.toNatPow`	—	`eval_single`
`eval_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `eval` `RingHom` `RingHom.instFunLike` `algebraMap` `map`	—	`induction_linear` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `map_single` `eval_single` `LinearMap.map_smul` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `algebraMap.coe_mul` `algebraMap.coe_pow` `algebraMap.coe_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat`
`eval_map'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `eval` `map`	—	`eval_map` `IsScalarTower.left`
`eval_single` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `eval` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `single` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Monoid.toNatPow`	—	`Finsupp.sum_single_index` `smul_zero`
`eval_smul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `eval` `Polynomial` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `polynomialModule` `Polynomial.eval`	—	`induction_linear` `smul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_add` `map_add` `SemilinearMapClass.toAddHomClass` `Polynomial.induction_on'` `add_smul` `Polynomial.eval_add` `monomial_smul_single` `eval_single` `Polynomial.eval_monomial` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat`
`hom_ext` 📖	—	`LinearMap.comp` `PolynomialModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lsingle`	—	—	`RingHomCompTriple.ids` `Finsupp.lhom_ext'`
`hom_ext_iff` 📖	mathematical	—	`LinearMap.comp` `PolynomialModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lsingle`	—	`RingHomCompTriple.ids` `hom_ext`
`induction_linear` 📖	—	`PolynomialModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupPolynomialModule` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `single`	—	—	`Finsupp.induction_linear`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `PolynomialModule` `Algebra.toSMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `instModule`	—	`Finsupp.isScalarTower`
`isScalarTower'` 📖	mathematical	—	`IsScalarTower` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PolynomialModule` `Algebra.toSMul` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `polynomialModule` `instModule`	—	`IsScalarTower.algebraMap_smul` `Polynomial.isScalarTower` `IsScalarTower.right` `instIsScalarTower` `smul_assoc` `Module.AEval.instIsScalarTowerOrigPolynomial`
`lsingle_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instFunLike` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `lsingle`	—	`Finsupp.single_apply`
`map_lsingle` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `map` `lsingle`	—	`map_single`
`map_single` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `map` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `single`	—	`Finsupp.mapRange_single` `LinearMap.map_zero`
`map_smul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `instModule` `LinearMap.instFunLike` `map` `Polynomial` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `polynomialModule` `Polynomial.map` `algebraMap`	—	`induction_linear` `smul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_add` `map_add` `SemilinearMapClass.toAddHomClass` `Polynomial.induction_on'` `add_smul` `Polynomial.map_add` `monomial_smul_single` `map_single` `Polynomial.map_monomial` `LinearMap.map_smul` `algebraMap_smul`
`monomial_smul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instFunLike` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PolynomialModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `polynomialModule` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.monomial`	—	`induction_linear` `smul_zero` `zero_apply` `smul_add` `add_apply` `zero_add` `monomial_smul_single` `single_apply` `smul_ite` `ite_and`
`monomial_smul_lsingle` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PolynomialModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `polynomialModule` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.monomial` `instModule` `lsingle`	—	`monomial_smul_single`
`monomial_smul_single` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PolynomialModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `polynomialModule` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.monomial` `AddMonoidHom` `AddMonoidHom.instFunLike` `single`	—	`Finsupp.smulCommClass` `smulCommClass_self` `Finsupp.isScalarTower` `IsScalarTower.left` `smul_def` `Polynomial.aeval_monomial` `Module.End.pow_apply` `Function.iterate_zero` `zero_add` `Finsupp.smul_single` `Function.iterate_succ` `add_assoc` `Finsupp.mapDomain_single`
`single_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instFunLike` `AddMonoidHom` `PolynomialModule` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `AddMonoidHom.instFunLike` `single`	—	`Finsupp.single_apply`
`single_smul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `PolynomialModule` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `AddMonoidHom.instFunLike` `single` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `instModule`	—	`LinearMap.map_smul`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instFunLike` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PolynomialModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `polynomialModule` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `Polynomial.coeff`	—	`Polynomial.induction_on'` `add_smul` `Finsupp.add_apply` `Finset.sum_add_distrib` `Polynomial.coeff_add` `Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `monomial_smul_apply` `Finset.sum_congr` `Polynomial.coeff_monomial` `Nat.instNoMaxOrder` `ite_smul` `zero_smul` `Finset.sum_ite_eq`
`smul_def` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PolynomialModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `polynomialModule` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `LinearMap.instFunLike` `AlgHom` `Module.End.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `Finsupp.smulCommClass` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Finsupp.isScalarTower` `IsScalarTower.left` `AlgHom.funLike` `Polynomial.aeval` `Finsupp.lmapDomain`	—	—
`smul_single_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instFunLike` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PolynomialModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupPolynomialModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `polynomialModule` `AddMonoidHom` `AddMonoidHom.instFunLike` `single` `Polynomial.coeff`	—	`Polynomial.induction_on'` `add_smul` `Finsupp.add_apply` `Polynomial.coeff_add` `zero_add`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instFunLike` `PolynomialModule` `instAddCommGroupPolynomialModule`	—	`Finsupp.zero_apply`

(root)

Definitions

Name	Category	Theorems
`PolynomialModule` 📖	CompOp	46 math math: `Ideal.Filtration.submodule_closure_single`, `Derivation.apply_eval_eq`, `Ideal.Filtration.submodule_eq_span_le_iff_stable_ge`, `taylorWithin_succ`, `PolynomialModule.comp_single`, `PolynomialModule.map_lsingle`, `PolynomialModule.smul_def`, `PolynomialModule.eval_map`, `PolynomialModule.map_smul`, `PolynomialModule.add_apply`, `PolynomialModule.comp_smul`, `PolynomialModule.aeval_equivPolynomial`, `Derivation.mapCoeffs_X`, `Ideal.Filtration.mem_submodule`, `PolynomialModule.monomial_smul_single`, `Derivation.mapCoeffs_C`, `PolynomialModule.single_smul`, `Derivation.mapCoeffs_monomial`, `PolynomialModule.single_apply`, `PolynomialModule.isScalarTower'`, `PolynomialModule.zero_apply`, `Ideal.Filtration.inf_submodule`, `PolynomialModule.comp_apply`, `Ideal.Filtration.submodule_span_single`, `PolynomialModule.eval_lsingle`, `PolynomialModule.smul_apply`, `PolynomialModule.equivPolynomial_single`, `PolynomialModule.smul_single_apply`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `PolynomialModule.equivPolynomialSelf_apply_eq`, `PolynomialModule.instIsScalarTower`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `PolynomialModule.lsingle_apply`, `PolynomialModule.eval_apply`, `PolynomialModule.eval_smul`, `PolynomialModule.comp_eval`, `Derivation.mapCoeffs_apply`, `PolynomialModule.monomial_smul_apply`, `Derivation.apply_aeval_eq'`, `PolynomialModule.monomial_smul_lsingle`, `PolynomialModule.eval_map'`, `PolynomialModule.hom_ext_iff`, `PolynomialModule.map_single`, `Ideal.Filtration.submodule_fg_iff_stable`, `PolynomialModule.eval_single`, `Derivation.apply_aeval_eq`
`instAddCommGroupPolynomialModule` 📖	CompOp	46 math math: `Ideal.Filtration.submodule_closure_single`, `Derivation.apply_eval_eq`, `Ideal.Filtration.submodule_eq_span_le_iff_stable_ge`, `taylorWithin_succ`, `PolynomialModule.comp_single`, `PolynomialModule.map_lsingle`, `PolynomialModule.smul_def`, `PolynomialModule.eval_map`, `PolynomialModule.map_smul`, `PolynomialModule.add_apply`, `PolynomialModule.comp_smul`, `PolynomialModule.aeval_equivPolynomial`, `Derivation.mapCoeffs_X`, `Ideal.Filtration.mem_submodule`, `PolynomialModule.monomial_smul_single`, `Derivation.mapCoeffs_C`, `PolynomialModule.single_smul`, `Derivation.mapCoeffs_monomial`, `PolynomialModule.single_apply`, `PolynomialModule.isScalarTower'`, `PolynomialModule.zero_apply`, `Ideal.Filtration.inf_submodule`, `PolynomialModule.comp_apply`, `Ideal.Filtration.submodule_span_single`, `PolynomialModule.eval_lsingle`, `PolynomialModule.smul_apply`, `PolynomialModule.equivPolynomial_single`, `PolynomialModule.smul_single_apply`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `PolynomialModule.equivPolynomialSelf_apply_eq`, `PolynomialModule.instIsScalarTower`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `PolynomialModule.lsingle_apply`, `PolynomialModule.eval_apply`, `PolynomialModule.eval_smul`, `PolynomialModule.comp_eval`, `Derivation.mapCoeffs_apply`, `PolynomialModule.monomial_smul_apply`, `Derivation.apply_aeval_eq'`, `PolynomialModule.monomial_smul_lsingle`, `PolynomialModule.eval_map'`, `PolynomialModule.hom_ext_iff`, `PolynomialModule.map_single`, `Ideal.Filtration.submodule_fg_iff_stable`, `PolynomialModule.eval_single`, `Derivation.apply_aeval_eq`
`instCoeFunPolynomialModuleForallNat` 📖	CompOp	—
`instFunLikePolynomialModuleNat` 📖	CompOp	—
`instInhabitedPolynomialModule` 📖	CompOp	—

---

← Back to Index