Documentation Verification Report

Derivation

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

Statistics

Metric	Count
Definitions `mkDerivation`, `mkDerivationEquiv`, `mkDerivationₗ`	3
Theorems `derivation_C`, `derivation_C_mul`, `derivation_eqOn_supported`, `derivation_eq_of_forall_mem_vars`, `derivation_eq_zero_of_forall_mem_vars`, `derivation_ext`, `derivation_ext_iff`, `leibniz_iff_X`, `mkDerivation_X`, `mkDerivation_monomial`, `mkDerivationₗ_C`, `mkDerivationₗ_X`, `mkDerivationₗ_monomial`	13
Total	16

MvPolynomial

Definitions

Name	Category	Theorems
`mkDerivation` 📖	CompOp	5 math math: `mkDerivation_X`, `pderiv_def`, `mkDerivation_monomial`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`
`mkDerivationEquiv` 📖	CompOp	—
`mkDerivationₗ` 📖	CompOp	3 math math: `mkDerivationₗ_monomial`, `mkDerivationₗ_C`, `mkDerivationₗ_X`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivation_C` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Derivation.map_algebraMap`
`derivation_C_mul` 📖	mathematical	—	`MvPolynomial` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `Module.toDistribMulAction` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `Derivation` `algebra` `Algebra.id` `Derivation.instFunLike`	—	`Derivation.leibniz` `derivation_C` `smul_zero` `add_zero` `C_mul'` `Derivation.map_smul`
`derivation_eqOn_supported` 📖	—	`Set.EqOn` `MvPolynomial` `DFunLike.coe` `Derivation` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `X` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `supported`	—	—	`Derivation.eqOn_adjoin` `Set.forall_mem_image`
`derivation_eq_of_forall_mem_vars` 📖	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `X`	—	—	`derivation_eqOn_supported` `mem_supported_vars`
`derivation_eq_zero_of_forall_mem_vars` 📖	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `X` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`derivation_eq_of_forall_mem_vars`
`derivation_ext` 📖	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `X`	—	—	`Derivation.ext` `derivation_eq_of_forall_mem_vars`
`derivation_ext_iff` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `X`	—	`derivation_ext`
`leibniz_iff_X` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `monomial` `X`	—	`C_eq_smul_one` `LinearMap.map_smul` `smul_zero` `induction_on'` `mul_one` `C_mul_monomial` `mul_assoc` `C_mul'` `smul_assoc` `smul_add` `SMulCommClass.smul_comm` `IsScalarTower.to_smulCommClass` `add_mul` `Distrib.rightDistribClass` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `add_smul` `add_add_add_comm` `induction_on` `mul_comm` `zero_add` `smul_one_smul` `mul_add` `Distrib.leftDistribClass` `Mathlib.Tactic.Abel.subst_into_add` `Mathlib.Tactic.Abel.term_atom` `Mathlib.Tactic.Abel.term_add_const` `Mathlib.Tactic.Abel.const_add_term` `SemigroupAction.mul_smul` `add_assoc` `smulCommClass_self`
`mkDerivation_X` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `mkDerivation` `X`	—	`mkDerivationₗ_X`
`mkDerivation_monomial` 📖	mathematical	—	`DFunLike.coe` `Derivation` `MvPolynomial` `commSemiring` `algebra` `Algebra.id` `Derivation.instFunLike` `mkDerivation` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finsupp.sum` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Finsupp.single` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mkDerivationₗ_monomial`
`mkDerivationₗ_C` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `mkDerivationₗ` `RingHom` `RingHom.instFunLike` `C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `mkDerivationₗ_monomial` `smul_zero`
`mkDerivationₗ_X` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `mkDerivationₗ` `X`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `mkDerivationₗ_monomial` `Finsupp.sum_single_index` `tsub_self` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.orderedSub` `Nat.cast_zero` `monomial_zero` `zero_smul` `Nat.cast_one` `one_smul`
`mkDerivationₗ_monomial` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `mkDerivationₗ` `monomial` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finsupp.sum` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Finsupp.single` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`sum_monomial_eq` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

---

← Back to Index