coe_norm_smul_basis — Mathlib

English

A variation of the norm formula for p, q ∈ R[X], interpreted through the AdjoinRoot representation of the coordinate ring; the same quadratic expression is obtained in the AdjoinRoot model.

Русский

Вариант формулы нормы для p, q ∈ R[X], трактуемый через представление CoordinateRing через AdjoinRoot; та же квадратичная формула получается в модели AdjoinRoot.

LaTeX

$$$\\text{coe\\_norm\\_smul\_basis}(p,q) = \\text{norm}_{R[X]}(p\\cdot 1 + q\\cdot \\mk_W' Y)$$$

Lean4

theorem coe_norm_smul_basis (p q : R[X]) :
    Algebra.norm R[X] (p • 1 + q • mk W' Y) =
      mk W' ((C p + C q * X) * (C p + C q * (-(Y : R[X][Y]) - C (C W'.a₁ * X + C W'.a₃)))) :=
  AdjoinRoot.mk_eq_mk.mpr ⟨C q ^ 2, by simp only [norm_smul_basis, polynomial]; C_simp; ring1⟩

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