Commit 2026-06-19 15:48 1b82673e

View on Github →

feat(RingTheory/Ideal/Over): add Ideal.smul_under (#40385) This PR proves g • P.under A = (g • P).under A in the SMulDistribClass setting.

Estimated changes

added theorem Ideal.smul_under
modified theorem Ideal.under_smul