Theorem Ideal.under_smul

Modification history

2024-10-28 23:09
Mathlib/RingTheory/Ideal/Over.lean
refactor(RingTheory/Ideal/Pointwise): Generalize to semirings (#18355) …
Added Ideal.under_smulView on Github →