Module

SeparablePolynomialFactors.lean

Nyll.ValuedFieldTheory.Valuation.Completion.SeparablePolynomialFactors

2 declarations indexed from sourceView source ↗

Module documentation

Distinct factors of a separable polynomial

A separable monic polynomial is the product of its distinct normalized irreducible factors, and those factors are pairwise coprime. These are the factorization facts used in the Chinese-remainder proof of tensor-product decomposition.

Imports2

Nyll.ValuedFieldTheory.Valuation.Completion.PolynomialFactors
Mathlib.FieldTheory.Separable

Imported by2

theorem

separable_monic_eq_prod_distinctNormalizedFactors

L30 ↗

ValuationTheory.Completion.separable_monic_eq_prod_distinctNormalizedFactors

Documentation

A monic separable polynomial is the product of its distinct normalized irreducible factors.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial UniqueFactorizationMonoid
open scoped BigOperators
namespace ValuationTheory
namespace Completion
universe u

Lean source · statement

theorem separable_monic_eq_prod_distinctNormalizedFactors
    {F : Type u} [Field F] (p : F[X])
    (hpmonic : p.Monic) (hpsep : p.Separable) :
    p = ∏ g : DistinctNormalizedFactors p, (g.1 : F[X])

theorem

distinctNormalizedFactors_pairwise_coprime

L55 ↗

ValuationTheory.Completion.distinctNormalizedFactors_pairwise_coprime