[GOAL]
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
⊢ Function.Injective ↑(RingHom.comp (Ideal.Quotient.mk I) C)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero _).2 fun x hx => _
[GOAL]
σ : 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
[PROOFSTEP]
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem] at hx 
[GOAL]
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
⊢ x = 0
[PROOFSTEP]
refine' _root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 _) hI
[GOAL]
σ : 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
[PROOFSTEP]
have := I.mul_mem_left (MvPolynomial.C x⁻¹) hx
[GOAL]
σ : 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
[PROOFSTEP]
rwa [← MvPolynomial.C.map_mul, inv_mul_cancel hx0, MvPolynomial.C_1] at this 
[GOAL]
σ K : Type u
inst✝ : Field K
⊢ Module.rank K (MvPolynomial σ K) = Cardinal.mk (σ →₀ ℕ)
[PROOFSTEP]
rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank]
