Theorem Submodule.index_smul_le

Modification history

2025-02-03 13:40
Mathlib/RingTheory/Ideal/Quotient/Index.lean
feat(RingTheory): index of power of ideal (#20290)
Added Submodule.index_smul_leView on Github →