Theorem Submodule.top_toAddSubgroup

Modification history

2025-11-24 14:10

Mathlib/Algebra/Module/Submodule/Lattice.lean

feat(Algebra): characterise when a quotient is nontrivial (#31198) …

Modified Submodule.top_toAddSubgroup View on Github →

2024-01-06 09:51

Mathlib/Algebra/Module/Submodule/Lattice.lean

feat: Provide glue between `AddCommGroup` and `Module ℤ` (#9345)

Added Submodule.top_toAddSubgroup View on Github →