no goals
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ n ∈ A (n • i)
match n with
| 0 =>
  rw [pow_zero, zero_nsmul]
  exact one_mem_graded _
| n+1 =>
  rw [pow_succ', succ_nsmul']
  exact mul_mem_graded (pow_mem_graded n h) h
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ 0 ∈ A (0 • i)
rw [pow_zero, zero_nsmul]
no goals
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0
exact one_mem_graded _
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ n * r ∈ A (n • i + i)
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ (n + 1) ∈ A ((n + 1) • i)
rw [pow_succ', succ_nsmul']
no goals
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ n * r ∈ A (n • i + i)
exact mul_mem_graded (pow_mem_graded n h) h