Commit 2024-07-02 14:16 2f44fc33

View on Github →

feat: add pointwise actions on ideals (#13294) I've copied the API from Subring, but some proofs from there don't work here due to Ideal.map including an extra Ideal.span.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Pointwise.lean

added theorem Ideal.mem_inv_pointwise_smul_iff

added theorem Ideal.mem_pointwise_smul_iff_inv_smul_mem

added theorem Ideal.pointwise_smul_def

added theorem Ideal.pointwise_smul_eq_comap

added theorem Ideal.pointwise_smul_le_pointwise_smul_iff

added theorem Ideal.pointwise_smul_subset_iff

added theorem Ideal.pointwise_smul_toAddSubGroup

added theorem Ideal.pointwise_smul_toAddSubmonoid

added theorem Ideal.smul_bot

added theorem Ideal.smul_closure

added theorem Ideal.smul_mem_pointwise_smul

added theorem Ideal.smul_mem_pointwise_smul_iff

added theorem Ideal.smul_sup

added theorem Ideal.subset_pointwise_smul_iff