mk_sub_mk

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.mk_sub_mk

English

Subtraction in 𝓞K is componentwise: (⟨x,hx⟩) − ⟨y,hy⟩ = ⟨x−y, sub_mem hx hy⟩.

Русский

Вычитание в 𝓞K по компонентам: (⟨x,hx⟩) − ⟨y,hy⟩ = ⟨x−y, sub_mem hx hy⟩.

LaTeX

$$$\\langle x,hx\\rangle - \\langle y,hy\\rangle = \\langle x-y, sub\\_mem hx hy\\rangle$$$

Lean4

@[simp]
theorem mk_sub_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) - ⟨y, hy⟩ = ⟨x - y, sub_mem hx hy⟩ :=
  rfl

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

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

Разделы

Аффилиация

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