Theorems · Definition · commutative algebra

Submodule.toAddSubgroup

{R : Type u} →
  {M : Type v} → [inst : Ring R] → [inst_1 : AddCommGroup M] → {module_M : Module R M} → Submodule R M → AddSubgroup M

Reinterpret a submodule as an additive subgroup.

Defined in

Mathlib.Algebra.Module.Submodule.Defs

Cited by

106 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 251 definitions · uses propext

Assumes

RingAddCommGroup