Documentation Verification Report

Polynomial

📁 Source: Mathlib/RingTheory/Kaehler/Polynomial.lean

Statistics

Metric	Count
Definitions `mvPolynomialBasis`, `mvPolynomialEquiv`, `polynomialEquiv`	3
Theorems `mvPolynomialBasis_apply`, `mvPolynomialBasis_repr_D`, `mvPolynomialBasis_repr_D_X`, `mvPolynomialBasis_repr_apply`, `mvPolynomialBasis_repr_comp_D`, `mvPolynomialBasis_repr_symm_single`, `polynomialEquiv_D`, `polynomialEquiv_comp_D`, `polynomialEquiv_symm`, `polynomial_D_apply`, `instFreeMvPolynomialKaehlerDifferential`	11
Total	14

KaehlerDifferential

Definitions

Name	Category	Theorems
`mvPolynomialBasis` 📖	CompOp	6 math math: `mvPolynomialBasis_apply`, `mvPolynomialBasis_repr_D_X`, `mvPolynomialBasis_repr_apply`, `mvPolynomialBasis_repr_D`, `mvPolynomialBasis_repr_comp_D`, `mvPolynomialBasis_repr_symm_single`
`mvPolynomialEquiv` 📖	CompOp	—
`polynomialEquiv` 📖	CompOp	3 math math: `polynomialEquiv_symm`, `polynomialEquiv_D`, `polynomialEquiv_comp_D`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mvPolynomialBasis_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `MvPolynomial` `CommRing.toCommSemiring` `KaehlerDifferential` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.algebra` `Algebra.id` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `module'` `Algebra.to_smulCommClass` `Module.Basis.instFunLike` `mvPolynomialBasis` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `MvPolynomial.X`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `mvPolynomialBasis_repr_symm_single` `one_smul`
`mvPolynomialBasis_repr_D` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `KaehlerDifferential` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.algebra` `Algebra.id` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module'` `Algebra.to_smulCommClass` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `mvPolynomialBasis` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `MvPolynomial.module` `MvPolynomial.mkDerivation` `Finsupp.isScalarTower` `MvPolynomial.smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NonUnitalNonAssocSemiring.toDistribSMul` `Algebra.toSMul` `IsScalarTower.right` `Finsupp.single` `AddMonoidWithOne.toOne`	—	`Derivation.congr_fun` `Algebra.to_smulCommClass` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `isScalarTower_of_tower` `IsScalarTower.right` `Finsupp.isScalarTower` `RingHomInvPair.ids` `mvPolynomialBasis_repr_comp_D`
`mvPolynomialBasis_repr_D_X` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `KaehlerDifferential` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.algebra` `Algebra.id` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module'` `Algebra.to_smulCommClass` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `mvPolynomialBasis` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `MvPolynomial.X` `Finsupp.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `Finsupp.isScalarTower` `IsScalarTower.right` `mvPolynomialBasis_repr_D` `MvPolynomial.mkDerivation_X`
`mvPolynomialBasis_repr_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MvPolynomial` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `KaehlerDifferential` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.algebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module'` `Algebra.to_smulCommClass` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `mvPolynomialBasis` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `MvPolynomial.module` `MvPolynomial.pderiv`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `isScalarTower_of_tower` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `MvPolynomial.derivation_ext` `mvPolynomialBasis_repr_D_X` `Finsupp.single_apply` `MvPolynomial.pderiv_X` `Pi.single_apply`
`mvPolynomialBasis_repr_comp_D` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Derivation` `KaehlerDifferential` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.algebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `module'` `Algebra.to_smulCommClass` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `MvPolynomial.module` `Derivation.instAddCommMonoid` `Derivation.instModule` `IsScalarTower.to_smulCommClass` `isScalarTower_of_tower` `Algebra.toSMul` `IsScalarTower.right` `CommSemiring.toCommMonoid` `Finsupp.isScalarTower` `MvPolynomial.smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NonUnitalNonAssocSemiring.toDistribSMul` `LinearMap.instFunLike` `LinearMap.compDer` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `Module.Basis.repr` `mvPolynomialBasis` `D` `MvPolynomial.mkDerivation` `Finsupp.single` `AddMonoidWithOne.toOne`	—	`Derivation.liftKaehlerDifferential_comp` `Finsupp.isScalarTower` `IsScalarTower.right`
`mvPolynomialBasis_repr_symm_single` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `KaehlerDifferential` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.algebra` `Algebra.id` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Finsupp.module` `Semiring.toModule` `module'` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `Module.Basis.repr` `mvPolynomialBasis` `Finsupp.single` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `MvPolynomial.X`	—	`LinearEquiv.injective` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `smulCommClass_self` `Module.Basis.repr_symm_apply` `Finsupp.linearCombination_single` `LinearEquiv.map_smul` `Module.Basis.repr_self` `Finsupp.smul_single` `mul_one` `mvPolynomialBasis_repr_D_X`
`polynomialEquiv_D` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `KaehlerDifferential` `Polynomial.commRing` `Polynomial.algebraOfAlgebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `module'` `Algebra.to_smulCommClass` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `polynomialEquiv` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `LinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.derivative`	—	`Derivation.congr_fun` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `isScalarTower_of_tower` `IsScalarTower.right` `polynomialEquiv_comp_D`
`polynomialEquiv_comp_D` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Derivation` `KaehlerDifferential` `Polynomial.commRing` `Polynomial.algebraOfAlgebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `module'` `Algebra.to_smulCommClass` `Polynomial.semiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Semiring.toModule` `Polynomial.module` `Derivation.instAddCommMonoid` `Derivation.instModule` `IsScalarTower.to_smulCommClass` `isScalarTower_of_tower` `Algebra.toSMul` `IsScalarTower.right` `CommSemiring.toCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.compDer` `polynomialEquiv` `D` `Polynomial.derivative'`	—	`Derivation.liftKaehlerDifferential_comp`
`polynomialEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `KaehlerDifferential` `Polynomial.commRing` `Polynomial.algebraOfAlgebra` `Algebra.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Semiring.toModule` `module'` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `polynomialEquiv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `Polynomial.X`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`polynomial_D_apply` 📖	mathematical	—	`DFunLike.coe` `Derivation` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `KaehlerDifferential` `Polynomial.commRing` `Polynomial.algebraOfAlgebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `module'` `Algebra.to_smulCommClass` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `D` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `Polynomial.X`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `Polynomial.aeval_X_left_apply` `Derivation.map_aeval`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFreeMvPolynomialKaehlerDifferential` 📖	mathematical	—	`Module.Free` `MvPolynomial` `CommRing.toCommSemiring` `KaehlerDifferential` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.algebra` `Algebra.id` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `KaehlerDifferential.module'` `Algebra.to_smulCommClass`	—	`Module.Free.of_basis` `Algebra.to_smulCommClass`

---

← Back to Index