norm_coe_units

Mathlib.Analysis.Normed.Ring.Int

URI: https://scilib.ai/kg/mathlib#Int.norm_coe_units

English

For a unit e in ℤˣ, the ordinary norm of e as an integer is 1: ∥e∥ = 1.

Русский

Для единицы в группе единиц ℤˣ нормa e как целого числа равна 1.

LaTeX

$$$\\|e\\| = 1 \\quad \\text{for } e \\in \\mathbb{Z}^{\\times}.$$$

Lean4

theorem norm_coe_units (e : ℤˣ) : ‖(e : ℤ)‖ = 1 := by rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]

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

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

Разделы

Аффилиация

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