Documentation Verification Report

DifferentialRing

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

Statistics

Metric	Count
Definitions `Differential`, `ContainConstants`, `deriv`, `equiv`, `«term_′»`, `DifferentialAlgebra`, `delabDeriv`	7
Theorems `mem_range_of_deriv_eq_zero`, `ext`, `ext_iff`, `deriv_algebraMap`, `equiv`, `coe_deriv`, `instContainConstants`, `instDifferentialAlgebra`, `mem_range_of_deriv_eq_zero`	9
Total	16

Differential

Definitions

Name	Category	Theorems
`ContainConstants` 📖	CompData	1 math math: `instContainConstants`
`deriv` 📖	CompOp	13 math math: `implicitDeriv_C`, `algHom_deriv`, `DifferentialAlgebra.deriv_algebraMap`, `algebraMap.coe_deriv`, `coeff_mapCoeffs`, `mapCoeffs_monomial`, `mapCoeffs_C`, `algHom_deriv'`, `deriv_aeval_eq`, `logDeriv_eq_zero`, `algEquiv_deriv'`, `ext_iff`, `algEquiv_deriv`
`equiv` 📖	CompOp	1 math math: `DifferentialAlgebra.equiv`
`«term_′»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`deriv`	—	—	—
`ext_iff` 📖	mathematical	—	`deriv`	—	`ext`

Differential.ContainConstants

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_range_of_deriv_eq_zero` 📖	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` `Differential.deriv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `algebraMap`	—	—

DifferentialAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv_algebraMap` 📖	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` `Differential.deriv` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—
`equiv` 📖	mathematical	—	`DifferentialAlgebra` `Differential.equiv` `AlgEquiv.toRingEquiv` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHomCompTriple.ids` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.commutes` `deriv_algebraMap`

(root)

Definitions

Name	Category	Theorems
`Differential` 📖	CompData	—
`DifferentialAlgebra` 📖	CompData	6 math math: `DifferentialAlgebra.equiv`, `Differential.instDifferentialAlgebraAdjoinRoot`, `instDifferentialAlgebra`, `Differential.differentialAlgebraFiniteDimensional`, `Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1`, `Differential.instDifferentialAlgebraSubtypeMemIntermediateField`
`delabDeriv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContainConstants` 📖	mathematical	—	`Differential.ContainConstants` `Algebra.id` `CommRing.toCommSemiring`	—	—
`instDifferentialAlgebra` 📖	mathematical	—	`DifferentialAlgebra` `Algebra.id` `CommRing.toCommSemiring`	—	—
`mem_range_of_deriv_eq_zero` 📖	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` `Differential.deriv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `algebraMap`	—	`Differential.ContainConstants.mem_range_of_deriv_eq_zero`

algebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_deriv` 📖	mathematical	—	`Algebra.cast` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `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` `Differential.deriv`	—	`DifferentialAlgebra.deriv_algebraMap`

---

← Back to Index