Module

MvPolynomial_mem_ideal_iff_forall_map_mem_map_localizationAway.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPolynomial_mem_ideal_iff_forall_map_mem_map_localizationAway

2 declarations indexed from sourceView source ↗

Module documentation

Mv Polynomial mem ideal iff forall map mem map localization Away

Imports3

Mathlib.RingTheory.Localization.Ideal
Mathlib.RingTheory.MvPolynomial.Localization
Mathlib.Tactic.Ring.RingNF

Imported by2

theorem

exists_pow_C_mul_mem

L32 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPolynomial_mem_ideal_iff_forall_map_mem_map_localizationAway.P3LocalMem.exists_pow_C_mul_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPolynomial_mem_ideal_iff_forall_map_mem_map_localizationAway
open MvPolynomial
namespace P3LocalMem
attribute [local instance] MvPolynomial.algebraMvPolynomial

Lean source · statement

theorem exists_pow_C_mul_mem {σ : Type} {A : Type} [CommRing A] (a : A)
    (I : Ideal (MvPolynomial σ A)) (f : MvPolynomial σ A)
    (h : MvPolynomial.map (algebraMap A (Localization.Away a)) f ∈
        Ideal.map (MvPolynomial.map (algebraMap A (Localization.Away a))) I) :
    ∃ n : ℕ, (C a : MvPolynomial σ A) ^ n * f ∈ I

theorem

mem_ideal_iff_forall_map_mem_map_localizationAway

L56 ↗

MvPolynomial.mem_ideal_iff_forall_map_mem_map_localizationAway

Source context 4 commands