Commit 2025-01-10 18:18 78b361bf

View on Github →

feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Differential/Basic.lean

added theorem Differential.differentialAlgebraFiniteDimensional

Created Mathlib/FieldTheory/Differential/Liouville.lean

added theorem IsLiouville.equiv

added theorem IsLiouville.trans

Modified Mathlib/RingTheory/Derivation/DifferentialRing.lean