coe_norm

Mathlib.NumberTheory.NumberField.Norm

URI: https://scilib.ai/kg/mathlib#RingOfIntegers.coe_norm

English

For x in 𝓞 L, the K-norm equals the K-norm of x considered in L: norm_K x = Algebra.norm_K (x : L).

Русский

Для x ∈ 𝓞 L нормa по K равна норме x, рассматриваемому как элемент L: \N_K(x) = \N_K(x \text{ в } L).

LaTeX

$$$\operatorname{norm}_K x = \operatorname{Algebra.norm}_K (x : L)$$$

Lean4

@[simp]
theorem coe_norm (x : 𝓞 L) : norm K x = Algebra.norm K (x : L) :=
  rfl

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

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

Разделы

Аффилиация

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