module Algebra.Ring.Module.Reasoning
{ℓ ℓm} {R : Ring ℓ}
(M : Module R ℓm)
whereReasoning with modules🔗
open Module-on (M .snd) public
Ab-group : Abelian-group ℓm
Ab-group = (M .fst , Module-on→Abelian-group-on (M .snd))module Algebra.Ring.Module.Reasoning
{ℓ ℓm} {R : Ring ℓ}
(M : Module R ℓm)
where open Module-on (M .snd) public
Ab-group : Abelian-group ℓm
Ab-group = (M .fst , Module-on→Abelian-group-on (M .snd))