mk'_num_den'

Mathlib.RingTheory.Localization.NumDen

URI: https://scilib.ai/kg/mathlib#IsFractionRing.mk'_num_den'

English

The two-tuple (num A x, den A x) localizes to x via mk' K.

Русский

Пара (num A x, den A x) локализуется в x через mk' K.

LaTeX

$$$\\mathrm{mk}'_K(\\mathrm{num}_A(x), \\mathrm{den}_A(x)) = x$$$

Lean4

@[simp]
theorem mk'_num_den' (x : K) : algebraMap A K (num A x) / algebraMap A K (den A x) = x :=
  by
  rw [← mk'_eq_div]
  apply mk'_num_den

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

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

Разделы

Аффилиация

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