rfl — Mathlib

English

Every field F is Liouville over itself: it carries the Liouville structure with a trivial primitive element construction.

Русский

Каждое поле F является Liouville над самим F: существует тривиальная конструкция Лиуильевой структуры.

LaTeX

$$$\\mathrm{IsLiouville} \\ F\\ F$$$

Lean4

instance rfl : IsLiouville F F where
  isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ x, (c x)′ = 0) (u : ι → F) (v : F)
    (h : a = ∑ x, c x * logDeriv (u x) + v′) := ⟨ι, _, c, hc, u, v, h⟩

Похожие утверждения