Commit 2024-10-21 16:18 340899eb

View on Github →

chore(Pointwise/Finset): move MonoidWithZero and Ring results out (#17999) Move them to two new files Algebra.GroupWithZero.Pointwise.Finset and Algebra.Ring.Pointwise.Finset

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

deleted theorem Finset.Nonempty.div_zero

deleted theorem Finset.Nonempty.mul_zero

deleted theorem Finset.Nonempty.smul_zero

deleted theorem Finset.Nonempty.zero_div

deleted theorem Finset.Nonempty.zero_mul

deleted theorem Finset.Nonempty.zero_smul

deleted theorem Finset.add_mul_subset

deleted theorem Finset.div_zero_subset

deleted theorem Finset.inv_op_smul_finset_distrib₀

deleted theorem Finset.inv_smul_finset_distrib₀

deleted theorem Finset.inv_smul_mem_iff₀

deleted theorem Finset.mem_inv_smul_finset_iff₀

deleted theorem Finset.mul_add_subset

deleted theorem Finset.mul_zero_subset

deleted theorem Finset.neg_smul_finset

deleted theorem Finset.smul_finset_inter₀

deleted theorem Finset.smul_finset_neg

deleted theorem Finset.smul_finset_sdiff₀

deleted theorem Finset.smul_finset_subset_iff₀

deleted theorem Finset.smul_finset_subset_smul_finset_iff₀

deleted theorem Finset.smul_finset_symmDiff₀

deleted theorem Finset.smul_finset_univ₀

deleted theorem Finset.smul_mem_smul_finset_iff₀

deleted theorem Finset.smul_univ₀'

deleted theorem Finset.smul_univ₀

deleted theorem Finset.smul_zero_subset

deleted theorem Finset.subset_smul_finset_iff₀

deleted theorem Finset.zero_div_subset

deleted theorem Finset.zero_mem_smul_finset

deleted theorem Finset.zero_mem_smul_finset_iff

deleted theorem Finset.zero_mem_smul_iff

deleted theorem Finset.zero_mul_subset

deleted theorem Finset.zero_smul_finset

deleted theorem Finset.zero_smul_finset_subset

deleted theorem Finset.zero_smul_subset

Created Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean

added theorem Finset.Nonempty.div_zero

added theorem Finset.Nonempty.mul_zero

added theorem Finset.Nonempty.smul_zero

added theorem Finset.Nonempty.zero_div

added theorem Finset.Nonempty.zero_mul

added theorem Finset.Nonempty.zero_smul

added theorem Finset.div_zero_subset

added theorem Finset.inv_op_smul_finset_distrib₀

added theorem Finset.inv_smul_finset_distrib₀

added theorem Finset.inv_smul_mem_iff₀

added theorem Finset.mem_inv_smul_finset_iff₀

added theorem Finset.mul_zero_subset

added theorem Finset.smul_finset_inter₀

added theorem Finset.smul_finset_neg

added theorem Finset.smul_finset_sdiff₀

added theorem Finset.smul_finset_subset_iff₀

added theorem Finset.smul_finset_subset_smul_finset_iff₀

added theorem Finset.smul_finset_symmDiff₀

added theorem Finset.smul_finset_univ₀

added theorem Finset.smul_mem_smul_finset_iff₀

added theorem Finset.smul_univ₀'

added theorem Finset.smul_univ₀

added theorem Finset.smul_zero_subset

added theorem Finset.subset_smul_finset_iff₀

added theorem Finset.zero_div_subset

added theorem Finset.zero_mem_smul_finset

added theorem Finset.zero_mem_smul_finset_iff

added theorem Finset.zero_mem_smul_iff

added theorem Finset.zero_mul_subset

added theorem Finset.zero_smul_finset

added theorem Finset.zero_smul_finset_subset

added theorem Finset.zero_smul_subset

Created Mathlib/Algebra/Ring/Pointwise/Finset.lean

added theorem Finset.add_mul_subset

added theorem Finset.mul_add_subset

added theorem Finset.neg_smul_finset