English
IsLiouville transfers along an algebra equivalence of fields, ensuring compatibility with the differential structure under the equivalence.
Русский
IsLiouville переносится вдоль алгебраического эквивалента полей, сохраняя совместимость с дифференциальной структурой под эквиваленцией.
LaTeX
$$$\\mathrm{IsLiouville}(F,K) \\Rightarrow \\mathrm{IsLiouville}(F,K')$$$
Lean4
/-- Transfer an `IsLiouville` instance using an equivalence `K ≃ₐ[F] K'`.
Requires an algebraic `K'` to show that the equivalence commutes with the derivative.
-/
theorem equiv {K' : Type*} [Field K'] [Differential K'] [Algebra F K'] [DifferentialAlgebra F K']
[Algebra.IsAlgebraic F K'] [inst : IsLiouville F K] (e : K ≃ₐ[F] K') : IsLiouville F K' where
isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ x, (c x)′ = 0) (u : ι → K') (v : K')
(h : a = ∑ x, c x * logDeriv (u x) +
v′) := by
apply inst.isLiouville a ι c hc (e.symm ∘ u) (e.symm v)
apply_fun e.symm at h
simpa [AlgEquiv.commutes, map_add, map_sum, map_mul, logDeriv, algEquiv_deriv'] using h
