Theorem: MvPolynomial.mk_eq_eval₂ (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
⊢ (↑↑(Ideal.Quotient.mk I)).toFun = eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) fun d => (Ideal.Quotient.mk I) (X d)
Tactic:
ext d
State after:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (↑↑(Ideal.Quotient.mk I)).toFun d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d

State before:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (↑↑(Ideal.Quotient.mk I)).toFun d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d
Tactic:
simp_rw [RingHom.toFun_eq_coe, ← mkₐ_eq_mk C, mkₐ_eq_aeval, aeval_X]
State after:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (aeval fun d => (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d

State before:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (aeval fun d => (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d
Tactic:
rfl
State after:
no goals