Documentation Verification Report

PDeriv

📁 Source: Mathlib/Algebra/MvPolynomial/PDeriv.lean

Statistics

Metric	Count
Definitions `pderiv`	1
Theorems `X_mul_pderiv_monomial`, `aeval_sumElim_pderiv_inl`, `pderiv_C`, `pderiv_C_mul`, `pderiv_X`, `pderiv_X_of_ne`, `pderiv_X_self`, `pderiv_def`, `pderiv_eq_zero_of_notMem_vars`, `pderiv_map`, `pderiv_monomial`, `pderiv_monomial_single`, `pderiv_mul`, `pderiv_one`, `pderiv_pow`, `pderiv_rename`, `pderiv_sumToIter`	17
Total	18

MvPolynomial

Definitions

Name	Category	Theorems
`pderiv` 📖	CompOp	39 math math: `Algebra.PreSubmersivePresentation.jacobiMatrix_naive`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_apply`, `IsWeightedHomogeneous.pderiv`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff`, `pderiv_one`, `pderiv_mul`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `Algebra.Generators.cotangentSpaceBasis_repr_one_tmul`, `pderiv_rename`, `X_mul_pderiv_monomial`, `pderiv_sumToIter`, `Algebra.PreSubmersivePresentation.jacobiMatrix_apply`, `Algebra.Generators.cotangentSpaceBasis_repr_tmul`, `Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation`, `pderiv_X`, `IsWeightedHomogeneous.sum_weight_X_mul_pderiv`, `pderiv_def`, `Algebra.PreSubmersivePresentation.aevalDifferential_single`, `KaehlerDifferential.mvPolynomialBasis_repr_apply`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `pderiv_C_mul`, `pderiv_monomial_single`, `pderiv_X_of_ne`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `pderiv_monomial`, `Algebra.Generators.repr_CotangentSpaceMap`, `pderiv_pow`, `pderiv_map`, `pderiv_inr_universalFactorizationMap_X`, `pderiv_eq_zero_of_notMem_vars`, `Algebra.Generators.cotangentRestrict_mk`, `IsHomogeneous.sum_X_mul_pderiv`, `aeval_sumElim_pderiv_inl`, `pderiv_X_self`, `pderiv_C`, `Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `IsHomogeneous.pderiv`, `Algebra.SubmersivePresentation.basisDeriv_apply`, `pderiv_inl_universalFactorizationMap_X`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_mul_pderiv_monomial` 📖	mathematical	—	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `X` `DFunLike.coe` `Derivation` `NonUnitalNonAssocSemiring.toAddCommMonoid` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `monomial` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pderiv_monomial` `X.eq_1` `monomial_mul` `smul_monomial` `Nat.cast_zero` `MulZeroClass.mul_zero` `zero_smul` `monomial_zero` `one_mul` `mul_comm` `nsmul_eq_mul` `add_comm` `Finsupp.sub_add_single_one_cancel`
`aeval_sumElim_pderiv_inl` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `Derivation` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv`	—	`induction_on` `derivation_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `algHom_C` `map_add` `AddMonoidHomClass.toAddHomClass` `Derivation.instAddMonoidHomClass` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Derivation.leibniz` `pderiv_X` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `aeval_X` `Pi.single_apply` `MonoidWithZeroHom.map_ite_one_zero` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Pi.single_eq_of_ne` `zero_add`
`pderiv_C` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `RingHom` `RingHom.instFunLike` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`derivation_C`
`pderiv_C_mul` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `C`	—	`C_mul'` `Derivation.map_smul`
`pderiv_X` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `X` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`IsScalarTower.right` `pderiv_def` `mkDerivation_X`
`pderiv_X_of_ne` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `X` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`pderiv_X` `Pi.single_eq_of_ne`
`pderiv_X_self` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `X` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`pderiv_X` `Pi.single_eq_same`
`pderiv_def` 📖	mathematical	—	`pderiv` `mkDerivation` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `module` `Semiring.toModule` `IsScalarTower.right` `algebra` `Algebra.id` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`IsScalarTower.right` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`pderiv_eq_zero_of_notMem_vars` 📖	mathematical	`Finset` `Finset.instMembership` `vars`	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`derivation_eq_zero_of_forall_mem_vars` `pderiv_X_of_ne`
`pderiv_map` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `RingHom` `RingHom.instFunLike` `map`	—	`induction_on` `map_C` `derivation_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `Derivation.instAddMonoidHomClass` `eq_or_ne` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_X` `Derivation.leibniz` `pderiv_X_self` `mul_one` `pderiv_X_of_ne` `MulZeroClass.mul_zero` `zero_add`
`pderiv_monomial` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Finsupp.single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finsupp.instFunLike`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `IsScalarTower.right` `pderiv_def` `mkDerivation_monomial` `Finsupp.smul_sum` `LinearMap.map_smul` `Finset.sum_eq_single` `Pi.single_eq_of_ne` `MulZeroClass.mul_zero` `Finsupp.notMem_support_iff` `Nat.cast_zero` `monomial_zero` `Pi.single_eq_same` `mul_one`
`pderiv_monomial_single` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `monomial` `Finsupp.single` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pderiv_monomial` `Finsupp.single_eq_same` `Finsupp.single_tsub`
`pderiv_mul` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd`	—	`Derivation.leibniz` `mul_comm` `add_comm`
`pderiv_one` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`pderiv_C`
`pderiv_pow` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Derivation.leibniz_pow` `nsmul_eq_mul` `smul_eq_mul` `mul_assoc`
`pderiv_rename` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `AlgHom` `AlgHom.funLike` `rename`	—	`induction_on` `algHom_C` `derivation_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AddMonoidHomClass.toAddHomClass` `Derivation.instAddMonoidHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `rename_X` `Derivation.leibniz` `pderiv_X` `Pi.single_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `zero_add`
`pderiv_sumToIter` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id` `Semiring.toModule` `module` `Derivation.instFunLike` `pderiv` `RingHom` `RingHom.instFunLike` `sumToIter`	—	`induction_on` `sumToIter_C` `derivation_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `Derivation.instAddMonoidHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `sumToIter_Xl` `Derivation.leibniz` `pderiv_X` `Pi.single_apply` `mul_one` `MulZeroClass.mul_zero` `sumToIter_Xr` `zero_add` `Pi.single_eq_of_ne`

---

← Back to Index