Theorem Submodule.finite_quotient_smul

Modification history

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