Finiteness of a ℤ-submodule read as an additive subgroup #
Submodule.toAddSubgroup is reducible and keeps the carrier set, so p and p.toAddSubgroup
have the same elements and the same ℤ-module structure. Instance search is nevertheless keyed
on the head symbol, so a Module.Finite ℤ p instance is never tried against the goal
Module.Finite ℤ p.toAddSubgroup. This file records that transfer once, for every ℤ-submodule,
rather than at each lattice presented to an API that reads additive subgroups.
Main declarations #
TauCeti.instModuleFiniteToAddSubgroup: a finitely generatedℤ-submodule stays finitely generated when read as an additive subgroup.
instance
TauCeti.instModuleFiniteToAddSubgroup
{M : Type u_1}
[AddCommGroup M]
(p : Submodule ℤ M)
[Module.Finite ℤ ↥p]
:
A finitely generated ℤ-submodule is still finitely generated when read as an additive
subgroup, the two being the same type.