MapCoeffs

📁 Source: Mathlib/RingTheory/Derivation/MapCoeffs.lean

Statistics

Metric	Count
Definitions mapCoeffs, implicitDeriv, mapCoeffs	3
Theorems apply_aeval_eq, apply_aeval_eq', apply_eval_eq, mapCoeffs_C, mapCoeffs_X, mapCoeffs_apply, mapCoeffs_monomial, algEquiv_deriv, algEquiv_deriv', algHom_deriv, algHom_deriv', coeff_mapCoeffs, deriv_aeval_eq, deriv_aeval_eq_implicitDeriv, implicitDeriv_C, implicitDeriv_X, mapCoeffs_C, mapCoeffs_X, mapCoeffs_monomial	19
Total	22

Derivation

Definitions

Name	Category	Theorems
mapCoeffs 📖	CompOp	9 math math: apply_eval_eq, mapCoeffs_X, mapCoeffs_C, mapCoeffs_monomial, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, mapCoeffs_apply, apply_aeval_eq', apply_aeval_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_aeval_eq 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap RingHom.id Semiring.toNonAssocSemiring PolynomialModule instAddCommGroupPolynomialModule PolynomialModule.instModule LinearMap.instFunLike PolynomialModule.eval Polynomial.commSemiring PolynomialModule.polynomialModule mapCoeffs compAlgebraMap SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule Polynomial.derivative	—	Finsupp.ext apply_aeval_eq'
apply_aeval_eq' 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Derivation instFunLike RingHom RingHom.instFunLike algebraMap	AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup PolynomialModule instAddCommGroupPolynomialModule PolynomialModule.instModule PolynomialModule.eval PolynomialModule.map Polynomial.commSemiring PolynomialModule.polynomialModule mapCoeffs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule Polynomial.derivative	—	Polynomial.induction_on' map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMonoidHomClass.toAddHomClass instAddMonoidHomClass LinearMap.semilinearMapClass add_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg Polynomial.aeval_monomial leibniz leibniz_pow mapCoeffs_monomial PolynomialModule.map_single PolynomialModule.eval_single Polynomial.derivative_monomial map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_natCast add_comm smul_smul Nat.cast_smul_eq_nsmul
apply_eval_eq 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike Polynomial.eval CommSemiring.toSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap RingHom.id Semiring.toNonAssocSemiring PolynomialModule instAddCommGroupPolynomialModule PolynomialModule.instModule LinearMap.instFunLike PolynomialModule.eval Polynomial Polynomial.commSemiring Polynomial.algebraOfAlgebra PolynomialModule.polynomialModule mapCoeffs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule Polynomial.derivative	—	apply_aeval_eq IsScalarTower.right IsScalarTower.left
mapCoeffs_C 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring PolynomialModule Polynomial.commSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Polynomial.algebraOfAlgebra PolynomialModule.polynomialModule PolynomialModule.instModule instFunLike mapCoeffs RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike PolynomialModule.single	—	mapCoeffs_monomial
mapCoeffs_X 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring PolynomialModule Polynomial.commSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Polynomial.algebraOfAlgebra PolynomialModule.polynomialModule PolynomialModule.instModule instFunLike mapCoeffs Polynomial.X NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mapCoeffs_monomial map_one_eq_zero map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
mapCoeffs_apply 📖	mathematical	—	DFunLike.coe Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instFunLike Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring PolynomialModule Polynomial.commSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Polynomial.algebraOfAlgebra PolynomialModule.polynomialModule PolynomialModule.instModule instFunLike mapCoeffs Polynomial.coeff	—	—
mapCoeffs_monomial 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring PolynomialModule Polynomial.commSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Polynomial.algebraOfAlgebra PolynomialModule.polynomialModule PolynomialModule.instModule instFunLike mapCoeffs LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Semiring.toModule Polynomial.module LinearMap.instFunLike Polynomial.monomial AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike PolynomialModule.single	—	Finsupp.ext Polynomial.coeff_monomial map_zero AddMonoidHomClass.toZeroHomClass instAddMonoidHomClass PolynomialModule.single_apply

Differential

Definitions

Name	Category	Theorems
implicitDeriv 📖	CompOp	3 math math: implicitDeriv_C, deriv_aeval_eq_implicitDeriv, implicitDeriv_X
mapCoeffs 📖	CompOp	5 math math: coeff_mapCoeffs, mapCoeffs_monomial, mapCoeffs_C, mapCoeffs_X, deriv_aeval_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquiv_deriv 📖	mathematical	IsSeparable CommRing.toRing	DFunLike.coe AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike Derivation Int.instCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.toIntAlgebra Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Derivation.instFunLike deriv	—	algHom_deriv Equiv.nontrivial IsDomain.toNontrivial AlgEquiv.injective
algEquiv_deriv' 📖	mathematical	—	DFunLike.coe AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike Derivation Int.instCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Derivation.instFunLike deriv	—	algHom_deriv' Equiv.nontrivial IsDomain.toNontrivial AlgEquiv.injective
algHom_deriv 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike IsSeparable CommRing.toRing	Derivation Int.instCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.toIntAlgebra Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Derivation.instFunLike deriv	—	mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Polynomial.aeval_algHom map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.Separable.aeval_derivative_ne_zero minpoly.aeval NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass add_left_cancel AddLeftCancelSemigroup.toIsLeftCancelAdd deriv_aeval_eq SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass map_zero AddMonoidHomClass.toZeroHomClass Derivation.instAddMonoidHomClass
algHom_deriv' 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	Derivation Int.instCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Derivation.instFunLike deriv	—	algHom_deriv Algebra.IsSeparable.isSeparable'
coeff_mapCoeffs 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe Derivation Polynomial Int.instCommSemiring Polynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.algebraOfAlgebra Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Polynomial.ring Derivation.instFunLike mapCoeffs deriv	—	—
deriv_aeval_eq 📖	mathematical	—	DFunLike.coe Derivation Int.instCommSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.toIntAlgebra CommRing.toRing Semiring.toModule CommSemiring.toSemiring AddCommGroup.toIntModule Ring.toAddCommGroup Derivation.instFunLike deriv AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Polynomial.commSemiring Polynomial.commRing Polynomial.ring mapCoeffs Distrib.toMul LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module LinearMap.instFunLike Polynomial.derivative	—	PolynomialModule.aeval_equivPolynomial Derivation.apply_aeval_eq' DifferentialAlgebra.deriv_algebraMap
deriv_aeval_eq_implicitDeriv 📖	mathematical	DFunLike.coe Derivation Int.instCommSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.toIntAlgebra CommRing.toRing Semiring.toModule CommSemiring.toSemiring AddCommGroup.toIntModule Ring.toAddCommGroup Derivation.instFunLike deriv AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	Polynomial.commSemiring Polynomial.commRing Polynomial.ring implicitDeriv	—	deriv_aeval_eq mul_comm map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass
implicitDeriv_C 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommSemiring Polynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.algebraOfAlgebra Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Polynomial.ring Derivation.instFunLike implicitDeriv RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C deriv	—	mapCoeffs_C Polynomial.derivation_C MulZeroClass.mul_zero add_zero
implicitDeriv_X 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommSemiring Polynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.algebraOfAlgebra Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Polynomial.ring Derivation.instFunLike implicitDeriv Polynomial.X	—	mapCoeffs_X Polynomial.derivative_X mul_one zero_add
mapCoeffs_C 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommSemiring Polynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.algebraOfAlgebra Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Polynomial.ring Derivation.instFunLike mapCoeffs RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C deriv	—	mapCoeffs_monomial
mapCoeffs_X 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommSemiring Polynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.algebraOfAlgebra Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Polynomial.ring Derivation.instFunLike mapCoeffs Polynomial.X Polynomial.instZero	—	mapCoeffs_monomial Derivation.map_one_eq_zero Polynomial.monomial_zero_right
mapCoeffs_monomial 📖	mathematical	—	DFunLike.coe Derivation Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommSemiring Polynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.algebraOfAlgebra Ring.toIntAlgebra CommRing.toRing Semiring.toModule AddCommGroup.toIntModule Ring.toAddCommGroup Polynomial.ring Derivation.instFunLike mapCoeffs LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module LinearMap.instFunLike Polynomial.monomial deriv	—	RingHomInvPair.ids Derivation.mapCoeffs_monomial

---

← Back to Index