of_apply

Mathlib.FieldTheory.PerfectClosure

URI: https://scilib.ai/kg/mathlib#PerfectClosure.of_apply

English

The embedding is given by the defining formula: for every x in K, PerfectClosure.of K p x equals mk K p (0, x).

Русский

Встроение задаётся формулой: для каждого x ∈ K, PerfectClosure.of K p x = mk K p (0, x).

LaTeX

$$$\forall x:\ K,\; \text{of}_{K,p}(x)=\mathrm{mk}(K,p)(0,x).$$$

Lean4

theorem of_apply (x : K) : of K p x = mk _ _ (0, x) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru