Theorems · Definition · commutative algebra

Polynomial.gaussNorm

{R : Type u_1} → {F : Type u_2} → [inst : Semiring R] → [FunLike F R ℝ] → F → ℝ → Polynomial R → ℝ

Given a polynomial p in R[X], a function v : R → ℝ and a real number c, the Gauss norm is defined as the supremum of the set of all values of v (p.coeff i) * c ^ i for all i in the support of p.

Defined in

Mathlib.RingTheory.Polynomial.GaussNorm

Cited by

20 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringFunLike