Theorems · Theorem · field theory

Polynomial.exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : NormedField L] [inst_2 : Algebra K L],
  DenseRange ⇑(algebraMap K L) →
    ∀ {f : Polynomial L},
      f.Monic →
        ∀ {ε : ℝ},
          ε > 0 →
            ∃ g,
              g.Monic ∧
                f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖(Polynomial.map (algebraMap K L) g).coeff n - f.coeff n‖ < ε

If K is a dense subfield of L, then every monic polynomial in L can be approximated by a monic polynomial in K of the same degree.

Defined in

Mathlib.Analysis.Normed.Field.Approximation

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNormedFieldAlgebra