Theorem Submodule.comap_smul_top_of_surjective

Modification history

2026-03-21 06:41
Mathlib/RingTheory/Ideal/Operations.lean
feat(RingTheory/Ideal): move and add some lemma about smul top (#36390) …
Added Submodule.comap_smul_top_of_surjectiveView on Github →