eq_iff

Mathlib.NumberTheory.NumberField.Basic

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

English

Equality in 𝓞K is detected by equality of the images in K.

Русский

Равенство в 𝓞K определяется равенством образов в K.

LaTeX

$$$(x : K) = (y : K) \\iff x = y$$$

Lean4

@[norm_cast]
theorem eq_iff {x y : 𝓞 K} : (x : K) = (y : K) ↔ x = y :=
  NumberField.RingOfIntegers.ext_iff.symm

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

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

Разделы

Аффилиация

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