Documentation Verification Report

Liouville

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

Statistics

Metric	Count
Definitions `IsLiouville`, `Liouville`	2
Theorems `equiv`, `isLiouville`, `rfl`, `trans`, `instIsLiouvilleSubtypeMemIntermediateField`, `isLiouville_of_finiteDimensional`	6
Total	8

IsLiouville

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv` 📖	mathematical	—	`IsLiouville`	—	`isLiouville` `Finset.sum_congr` `AlgEquiv.commutes` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Differential.algEquiv_deriv'` `instIsDomain` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `PerfectField.ofCharZero`
`isLiouville` 📖	—	`DFunLike.coe` `Derivation` `Int.instCommSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `Algebra.cast` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Finset.sum` `Finset.univ` `Distrib.toMul` `Differential.logDeriv`	—	—	—
`rfl` 📖	mathematical	—	`IsLiouville` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	—
`trans` 📖	mathematical	—	`IsLiouville`	—	`isLiouville` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finset.sum_congr` `mem_range_of_deriv_eq_zero` `FaithfulSMul.algebraMap_injective` `algebraMap.coe_deriv` `algebraMap.coe_zero`

(root)

Definitions

Name	Category	Theorems
`IsLiouville` 📖	CompData	5 math math: `IsLiouville.rfl`, `instIsLiouvilleSubtypeMemIntermediateField`, `isLiouville_of_finiteDimensional`, `IsLiouville.trans`, `IsLiouville.equiv`
`Liouville` 📖	MathDef	9 math math: `dense_liouville`, `volume_setOf_liouville`, `forall_liouvilleWith_iff`, `IsGδ.setOf_liouville`, `setOf_liouville_eq_iInter_iUnion`, `ae_not_liouville`, `liouville_liouvilleNumber`, `eventually_residual_liouville`, `setOf_liouville_eq_irrational_inter_iInter_iUnion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLiouvilleSubtypeMemIntermediateField` 📖	mathematical	—	`IsLiouville` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `Differential.instSubtypeMemIntermediateFieldOfFiniteDimensional` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `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` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `IsLiouville.isLiouville` `Differential.logDeriv_algebraMap` `Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1` `DifferentialAlgebra.deriv_algebraMap` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.algebraMap_apply` `IntermediateField.isScalarTower_mid'` `Finset.sum_congr` `IntermediateField.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isLiouville_of_finiteDimensional` 📖	mathematical	—	`IsLiouville`	—	`AlgebraicClosure.isAlgClosed` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsSeparable.of_integral` `Algebra.IsIntegral.of_finite` `PerfectField.ofCharZero` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `LinearMap.finiteDimensional_range` `IntermediateField.le_normalClosure` `IntermediateField.isScalarTower` `IsLiouville.equiv` `IntermediateField.finiteDimensional_left` `normalClosure.is_finiteDimensional` `Differential.instDifferentialAlgebraSubtypeMemIntermediateField` `instIsLiouvilleSubtypeMemIntermediateField` `IsGalois.normalClosure` `IsAlgClosure.isGalois` `AlgebraicClosure.instIsAlgClosureOfIsAlgebraic` `Normal.toIsAlgebraic` `normal_self`

---

← Back to Index