Theorem: DividedPowerAlgebra.proj'_zero_mul (DividedPowers/DPAlgebra/Graded/Basic.lean)

State before:
R : Type u_1
M : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : DecidableEq R
inst✝⁸ : DecidableEq M
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x y : DividedPowerAlgebra R M
⊢ (proj' R M 0) (x * y) = (proj' R M 0) x * (proj' R M 0) y
Tactic:
simp only [proj', ← projZeroRingHom'_apply, _root_.map_mul]
State after:
no goals