norm_intCast

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.norm_intCast

English

Let n be an integer. When viewed as an element of Z[√d], its norm equals n^2.

Русский

Пусть n целое число. Рассматривая n как элемент ℤ√d, норма равна n^2.

LaTeX

$$$\\operatorname{norm}(n) = n^2, \\quad n \\in \\mathbb{Z}$$$

Lean4

@[simp]
theorem norm_intCast (n : ℤ) : norm (n : ℤ√d) = n * n := by simp [norm]

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

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

Разделы

Аффилиация

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