Theorem Ideal.pointwise_smul_toAddSubGroup

Modification history

2024-10-28 23:09
Mathlib/RingTheory/Ideal/Pointwise.lean
refactor(RingTheory/Ideal/Pointwise): Generalize to semirings (#18355) …
Modified Ideal.pointwise_smul_toAddSubGroupView on Github →
2024-07-02 14:16
Mathlib/RingTheory/Ideal/Pointwise.lean
feat: add pointwise actions on ideals (#13294) …
Added Ideal.pointwise_smul_toAddSubGroupView on Github →