case intro
ι : Type u_1
R : Type ?u.161779
A : Type u_2
σ : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : { x // x ∈ 𝒜 j }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) (i + j)) = ↑(↑(↑(decompose 𝒜) a) i) * ↑b
ι : Type u_1
R : Type ?u.161779
A : Type u_2
σ : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) (i + j)) = ↑(↑(↑(decompose 𝒜) a) i) * b
lift b to 𝒜 j using b_mem
no goals
case intro
ι : Type u_1
R : Type ?u.161779
A : Type u_2
σ : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : { x // x ∈ 𝒜 j }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) (i + j)) = ↑(↑(↑(decompose 𝒜) a) i) * ↑b
rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]