no goals
ι : Type u_1
σ : Type ?u.561128
S : Type u_2
R : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : { x // x ∈ A i }
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) 0) GradedMonoid.GOne.one = 1
rfl
no goals
ι : Type u_1
σ : Type ?u.561128
S : Type u_2
R : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : { x // x ∈ A i }
i✝ j✝ : ι
x✝¹ : { x // x ∈ A i✝ }
x✝ : { x // x ∈ A j✝ }
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) (i✝ + j✝))
      (GradedMonoid.GMul.mul x✝¹ x✝) =
    ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) i✝) x✝¹ *
      ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) j✝) x✝
rfl