σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑(RingHom.comp (Ideal.Quotient.mk I) C) x = 0
⊢ x = 0
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
⊢ Function.Injective ↑(RingHom.comp (Ideal.Quotient.mk I) C)
refine' (injective_iff_map_eq_zero _).2 fun x hx => _
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
⊢ x = 0
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑(RingHom.comp (Ideal.Quotient.mk I) C) x = 0
⊢ x = 0
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem] at hx
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
⊢ x = 0
refine' _root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 _) hI
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
hx0 : ¬x = 0
this : ↑C x⁻¹ * ↑C x ∈ I
⊢ 1 ∈ I
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I
have := I.mul_mem_left (MvPolynomial.C x⁻¹) hx
no goals
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
hx0 : ¬x = 0
this : ↑C x⁻¹ * ↑C x ∈ I
⊢ 1 ∈ I
rwa [← MvPolynomial.C.map_mul, inv_mul_cancel hx0, MvPolynomial.C_1] at this