ModuleKummerEisenstein.lean
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.KummerEisenstein
2 declarations indexed from sourceView source ↗ Module documentation
Eisenstein binomials from a prime parameter
A positive-power binomial X ^ n - C π is Eisenstein at the principal ideal of a prime element. In an integrally closed domain, its image in the fraction field is therefore irreducible. These inputs require no valuation, residue-field comparison, or prescribed extension degree.
Imports8
- Mathlib.Algebra.GroupWithZero.Divisibility
- Mathlib.Algebra.Polynomial.Coeff
- Mathlib.Algebra.Polynomial.Degree.Operations
- Mathlib.Algebra.Polynomial.Monic
- Mathlib.RingTheory.Ideal.Operations
- Mathlib.RingTheory.Ideal.Span
- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
- Mathlib.RingTheory.Polynomial.GaussLemma
Imported by2
Declarations
ValuationTheory.DiscreteValuationField.X_pow_sub_C_isEisensteinAt_of_prime_parameter
DocumentationA prime parameter makes a positive-power binomial Eisenstein.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u v
variable {R : Type u} [CommRing R] [IsDomain R]
ValuationTheory.DiscreteValuationField.X_pow_sub_C_irreducible_of_prime_parameter
DocumentationThe Eisenstein binomial is irreducible over the fraction field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u v
variable {R : Type u} [CommRing R] [IsDomain R]