Theorem Submodule.toIntSubmodule_toAddSubgroup

Modification history

2025-06-14 13:55
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
feat(NumberTheory): discriminant is norm of different (#25792)
Added Submodule.toIntSubmodule_toAddSubgroupView on Github →