English
For any A, i, x ∈ A i, and n ∈ ℕ, the coercion of gnpow n x equals x^n in R.
Русский
Для A, i и x ∈ A i, и n ∈ ℕ, приведение gnpow n x равно x^n в R.
LaTeX
$$$\\uparrow(\\mathrm{GMonoid.Gnpow}\ n\ x) = x^n$$$
Lean4
/-- Build a `GMonoid` instance for a collection of subobjects. -/
instance gMonoid {S : Type*} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] :
GradedMonoid.GMonoid fun i => A i :=
{ SetLike.gOne A,
SetLike.gMul A with
one_mul := fun ⟨_, _, _⟩ => Sigma.subtype_ext (zero_add _) (one_mul _)
mul_one := fun ⟨_, _, _⟩ => Sigma.subtype_ext (add_zero _) (mul_one _)
mul_assoc := fun ⟨_, _, _⟩ ⟨_, _, _⟩ ⟨_, _, _⟩ => Sigma.subtype_ext (add_assoc _ _ _) (mul_assoc _ _ _)
gnpow := fun n _ a => ⟨(a : R) ^ n, SetLike.pow_mem_graded n a.prop⟩
gnpow_zero' := fun _ => Sigma.subtype_ext (zero_nsmul _) (pow_zero _)
gnpow_succ' := fun _ _ => Sigma.subtype_ext (succ_nsmul _ _) (pow_succ _ _) }
