Documentation Verification Report

Basic

📁 Source: Mathlib/FieldTheory/Differential/Basic.lean

Statistics

Metric	Count
Definitions `differentialFiniteDimensional`, `instAdjoinRootOfIrreduciblePolynomialOfFactMonic`, `instSubtypeMemIntermediateFieldOfFiniteDimensional`, `logDeriv`, `uniqueDifferentialAlgebraFiniteDimensional`	5
Theorems `differentialAlgebraFiniteDimensional`, `instDifferentialAlgebraAdjoinRoot`, `instDifferentialAlgebraSubtypeMemIntermediateField`, `instDifferentialAlgebraSubtypeMemIntermediateField_1`, `logDeriv_algebraMap`, `logDeriv_div`, `logDeriv_eq_zero`, `logDeriv_mul`, `logDeriv_multisetProd`, `logDeriv_one`, `logDeriv_pow`, `logDeriv_prod`, `logDeriv_prod_of_eq_zero`, `logDeriv_zero`, `coe_logDeriv`	15
Total	20

Differential

Definitions

Name	Category	Theorems
`differentialFiniteDimensional` 📖	CompOp	1 math math: `differentialAlgebraFiniteDimensional`
`instAdjoinRootOfIrreduciblePolynomialOfFactMonic` 📖	CompOp	1 math math: `instDifferentialAlgebraAdjoinRoot`
`instSubtypeMemIntermediateFieldOfFiniteDimensional` 📖	CompOp	3 math math: `instIsLiouvilleSubtypeMemIntermediateField`, `instDifferentialAlgebraSubtypeMemIntermediateField_1`, `instDifferentialAlgebraSubtypeMemIntermediateField`
`logDeriv` 📖	CompOp	11 math math: `logDeriv_prod`, `algebraMap.coe_logDeriv`, `logDeriv_prod_of_eq_zero`, `logDeriv_div`, `logDeriv_one`, `logDeriv_mul`, `logDeriv_zero`, `logDeriv_pow`, `logDeriv_algebraMap`, `logDeriv_eq_zero`, `logDeriv_multisetProd`
`uniqueDifferentialAlgebraFiniteDimensional` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentialAlgebraFiniteDimensional` 📖	mathematical	—	`DifferentialAlgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `differentialFiniteDimensional`	—	`Field.exists_primitive_element` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `PerfectField.ofCharZero` `DifferentialAlgebra.equiv` `instDifferentialAlgebraAdjoinRoot`
`instDifferentialAlgebraAdjoinRoot` 📖	mathematical	—	`DifferentialAlgebra` `AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AdjoinRoot.instCommRing` `AdjoinRoot.instAlgebra` `CommRing.toCommSemiring` `Algebra.id` `instAdjoinRootOfIrreduciblePolynomialOfFactMonic`	—	`Derivation.liftOfSurjective_apply` `implicitDeriv_C`
`instDifferentialAlgebraSubtypeMemIntermediateField` 📖	mathematical	—	`DifferentialAlgebra` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `instSubtypeMemIntermediateFieldOfFiniteDimensional`	—	`IsScalarTower.left` `differentialAlgebraFiniteDimensional`
`instDifferentialAlgebraSubtypeMemIntermediateField_1` 📖	mathematical	—	`DifferentialAlgebra` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield` `instSubtypeMemIntermediateFieldOfFiniteDimensional`	—	`IsScalarTower.left` `algHom_deriv'` `instDifferentialAlgebraSubtypeMemIntermediateField` `instIsDomain` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsSeparable.isAlgebraic` `Algebra.IsSeparable.of_integral` `Algebra.IsIntegral.of_finite` `PerfectField.ofCharZero` `Subtype.val_injective`
`logDeriv_algebraMap` 📖	mathematical	—	`logDeriv` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap`	—	`DifferentialAlgebra.deriv_algebraMap` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`logDeriv_div` 📖	mathematical	—	`logDeriv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`Derivation.leibniz_div` `inv_pow` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`logDeriv_eq_zero` 📖	mathematical	—	`logDeriv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `Derivation` `Int.instCommSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Ring.toIntAlgebra` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `Derivation.instFunLike` `deriv`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `Derivation.instAddMonoidHomClass` `zero_div`
`logDeriv_mul` 📖	mathematical	—	`logDeriv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd`	—	`Derivation.leibniz` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt`
`logDeriv_multisetProd` 📖	mathematical	—	`logDeriv` `Multiset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Multiset.map` `Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Multiset.induction_on` `logDeriv_one` `Multiset.map_cons` `Multiset.prod_cons` `Multiset.sum_cons` `logDeriv_mul` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`logDeriv_one` 📖	mathematical	—	`logDeriv` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Derivation.map_one_eq_zero` `div_one`
`logDeriv_pow` 📖	mathematical	—	`logDeriv` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`pow_zero` `logDeriv_one` `Nat.cast_zero` `MulZeroClass.zero_mul` `eq_or_ne` `zero_pow` `logDeriv_zero` `Nat.cast_add` `Nat.cast_one` `MulZeroClass.mul_zero` `add_mul` `Distrib.rightDistribClass` `one_mul` `pow_succ` `logDeriv_mul` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`logDeriv_prod` 📖	mathematical	—	`logDeriv` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`logDeriv_multisetProd`
`logDeriv_prod_of_eq_zero` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`logDeriv` `Finset.prod` `CommRing.toCommMonoid` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.prod_congr` `Finset.prod_const` `Derivation.leibniz_pow` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Derivation.instAddMonoidHomClass` `MulZeroClass.mul_zero` `nsmul_zero` `zero_div` `Finset.sum_congr` `div_zero` `Finset.sum_const_zero`
`logDeriv_zero` 📖	mathematical	—	`logDeriv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `Derivation.instAddMonoidHomClass` `div_zero`

algebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_logDeriv` 📖	mathematical	—	`Algebra.cast` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Differential.logDeriv`	—	`Differential.logDeriv_algebraMap`

---

← Back to Index