case intro
ι : Type u_3
R : Type ?u.341327
A : Type u_1
σ : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = 0
ι : Type u_3
R : Type ?u.341327
A : Type u_1
σ : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = 0
lift a to 𝒜 i using a_mem
no goals
case intro
ι : Type u_3
R : Type ?u.341327
A : Type u_1
σ : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = 0
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]