Module

Polynomial_exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Polynomial_exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq

2 declarations indexed from sourceView source ↗

Module documentation

Polynomial exists is Unit aeval of sub mem maximal Ideal imp eq

Imports2

Mathlib.Algebra.Polynomial.Roots
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by3

theorem

exists_isUnit_aeval

L37 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Polynomial_exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq.Polynomial.GoodValueImpl.exists_isUnit_aeval

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Polynomial_exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq
universe u
open _root_.Polynomial
open _root_.IsLocalRing
namespace Polynomial
open _root_.Polynomial
namespace GoodValueImpl
open _root_.Polynomial
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] [IsLocalRing S]

Lean source · statement

theorem exists_isUnit_aeval (D : Polynomial R) (hD : ∃ i, IsUnit (D.coeff i))
    (x : Fin (D.natDegree + 1) → S) (hx : ∀ i j, x i - x j ∈ IsLocalRing.maximalIdeal S → i = j) :
    ∃ i, IsUnit (Polynomial.aeval (x i) D)

theorem

exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq

L79 ↗

Polynomial.exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq

Source context 6 commands