Theorem: MvPolynomial.mkₐ_eq_aeval (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)
⊢ mkₐ C I = aeval fun d => (Ideal.Quotient.mk I) (X d)
Tactic:
ext d
State after:
case hf
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 : D
⊢ (mkₐ C I) (X d) = (aeval fun d => (Ideal.Quotient.mk I) (X d)) (X d)

State before:
case hf
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 : D
⊢ (mkₐ C I) (X d) = (aeval fun d => (Ideal.Quotient.mk I) (X d)) (X d)
Tactic:
simp only [mkₐ_eq_mk, aeval_X]
State after:
no goals