Commit 2023-10-16 13:44 e3644b2c

feat: add a Module.Finite instance for units of number field (#7412) Add the following instance

instance : Module.Finite ℤ (Additive (𝓞 K)ˣ)

To prove this instance, it is helpful to add some rfl lemmas about Additive and AddMonoidHom.toIntLinearMap This PR also fixes a couple of typo in the docstring

Estimated changes

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem AddSubgroup.toSubgroup_comap

added theorem MonoidHom.coe_toAdditive_ker

added theorem MonoidHom.coe_toAdditive_range

added theorem MonoidHom.coe_toMultiplicative_ker

added theorem MonoidHom.coe_toMultiplicative_range

added theorem Subgroup.toAddSubgroup_comap

Modified Mathlib/LinearAlgebra/Basic.lean

added theorem AddMonoidHom.coe_toIntLinearMap_ker

added theorem AddMonoidHom.coe_toIntLinearMap_map

added theorem AddMonoidHom.coe_toIntLinearMap_range

added theorem AddMonoidHom.coe_toMultiplicative_map

added theorem MonoidHom.coe_toAdditive_map

added theorem Submodule.AddMonoidHom.coe_toIntLinearMap_comap

Modified Mathlib/NumberTheory/NumberField/Units.lean

modified theorem NumberField.Units.dirichletUnitTheorem.exists_unit