quot_mk_eq_mk

Mathlib.FieldTheory.PerfectClosure

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

English

The quotient mk of a pair is equal to the canonical PerfectClosure representation of that pair.

Русский

Квадратный эквивалент mk пары равен каноническому представлению PerfectClosure этой пары.

LaTeX

$$$(\mathrm{Quot.mk} (\mathrm{R}\;K\;p) x) = \mathrm{mk}\;K\;p\; x$$$

Lean4

@[simp]
theorem quot_mk_eq_mk (x : ℕ × K) : (Quot.mk (R K p) x : PerfectClosure K p) = mk K p x :=
  rfl

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

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

Разделы

Аффилиация

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