Commit 2021-11-23 07:23 ca7347c4

View on Github →

refactor(ring_theory/sub[semi]ring): move pointwise instances to their own file (#10347) This matches how we have separate pointwise files for submonoid and subgroup. All the new lemmas are direct copies of the subgroup lemmas.

Estimated changes

Modified counterexamples/canonically_ordered_comm_semiring_two_mul.lean

Modified src/algebra/algebra/subalgebra.lean

Modified src/algebra/category/CommRing/limits.lean

Modified src/algebra/char_p/subring.lean

Modified src/algebra/group_ring_action.lean

deleted theorem subring.coe_pointwise_smul

deleted theorem subring.pointwise_smul_to_add_subgroup

deleted theorem subring.pointwise_smul_to_subsemiring

deleted theorem subring.smul_mem_pointwise_smul

deleted theorem subsemiring.coe_pointwise_smul

deleted theorem subsemiring.pointwise_smul_to_add_submonoid

deleted theorem subsemiring.smul_mem_pointwise_smul

Modified src/algebraic_geometry/structure_sheaf.lean

Modified src/deprecated/subring.lean

Modified src/ring_theory/perfection.lean

Renamed src/ring_theory/subring.lean to src/ring_theory/subring/basic.lean

Created src/ring_theory/subring/pointwise.lean

added theorem subring.coe_pointwise_smul

added theorem subring.le_pointwise_smul_iff₀

added theorem subring.mem_inv_pointwise_smul_iff

added theorem subring.mem_inv_pointwise_smul_iff₀

added theorem subring.mem_pointwise_smul_iff_inv_smul_mem

added theorem subring.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem subring.pointwise_smul_def

added theorem subring.pointwise_smul_le_iff₀

added theorem subring.pointwise_smul_le_pointwise_smul_iff

added theorem subring.pointwise_smul_le_pointwise_smul_iff₀

added theorem subring.pointwise_smul_subset_iff

added theorem subring.pointwise_smul_to_add_subgroup

added theorem subring.pointwise_smul_to_subsemiring

added theorem subring.smul_mem_pointwise_smul

added theorem subring.smul_mem_pointwise_smul_iff

added theorem subring.smul_mem_pointwise_smul_iff₀

added theorem subring.subset_pointwise_smul_iff

Renamed src/ring_theory/subsemiring.lean to src/ring_theory/subsemiring/basic.lean

Created src/ring_theory/subsemiring/pointwise.lean

added theorem subsemiring.coe_pointwise_smul

added theorem subsemiring.le_pointwise_smul_iff₀

added theorem subsemiring.mem_inv_pointwise_smul_iff

added theorem subsemiring.mem_inv_pointwise_smul_iff₀

added theorem subsemiring.mem_pointwise_smul_iff_inv_smul_mem

added theorem subsemiring.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem subsemiring.pointwise_smul_def

added theorem subsemiring.pointwise_smul_le_iff₀

added theorem subsemiring.pointwise_smul_le_pointwise_smul_iff

added theorem subsemiring.pointwise_smul_le_pointwise_smul_iff₀

added theorem subsemiring.pointwise_smul_subset_iff

added theorem subsemiring.pointwise_smul_to_add_submonoid

added theorem subsemiring.smul_mem_pointwise_smul

added theorem subsemiring.smul_mem_pointwise_smul_iff

added theorem subsemiring.smul_mem_pointwise_smul_iff₀

added theorem subsemiring.subset_pointwise_smul_iff

Modified src/topology/algebra/ring.lean

Modified src/topology/instances/real.lean