English
Liouville property is preserved under algebraic equivalence: if K is Liouville over F and e: K ≃ₐ[F] K' is an algebra isomorphism, then K' is Liouville over F.
Русский
Свойство Liouville сохраняется под алгебраическими эквивалентами: если K Liouville над F и e: K ≃ₐ[F] K', то K' тоже Liouville над F.
LaTeX
$$$\\mathrm{IsLiouville}(F,K) \\to (e : K \\simeq_A[F] K') \\Rightarrow \\mathrm{IsLiouville}(F,K')$$$
Lean4
/-- If `K` is a Liouville extension of `F` and `B` is a finite-dimensional intermediate
field `K / B / F`, then it's also a Liouville extension of `F`.
-/
instance (B : IntermediateField F K) [FiniteDimensional F B] [inst : IsLiouville F K] : IsLiouville F B where
isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ x, (c x)′ = 0) (u : ι → B) (v : B)
(h : a = ∑ x, c x * logDeriv (u x) +
v′) := by
apply inst.isLiouville a ι c hc (B.val ∘ u) (B.val v)
dsimp only [coe_val, Function.comp_apply]
conv =>
rhs
congr
· rhs
intro x
rhs
apply logDeriv_algebraMap (u x)
· apply (deriv_algebraMap v)
simp_rw [IsScalarTower.algebraMap_apply F B K]
norm_cast
