Theorem Ideal.smul_under

Modification history

2026-06-19 15:48
Mathlib/RingTheory/Ideal/Over.lean
feat(RingTheory/Ideal/Over): add `Ideal.smul_under` (#40385) …
Added Ideal.smul_underView on Github →