Commit 2024-09-04 18:26 22f19a64

View on Github →

chore: Split Data.Set.Pointwise.Basic (#16442) ... into

  • Algebra.Group.Pointwise.Set for Group properties
  • Algebra.GroupWithZero.Pointwise.Set for GroupWithZero properties
  • Algebra.Ring.Pointwise.Set for HasDistribNeg and Distrib properties Other files under Data.Set.Pointwise will follow later

Estimated changes

deleted theorem Set.Nonempty.div_zero
deleted theorem Set.Nonempty.mul_zero
deleted theorem Set.Nonempty.zero_div
deleted theorem Set.Nonempty.zero_mul
deleted theorem Set.add_mul_subset
deleted theorem Set.div_zero_subset
deleted theorem Set.mul_add_subset
deleted theorem Set.mul_zero_subset
deleted theorem Set.zero_div_subset
deleted theorem Set.zero_mul_subset
added theorem Set.Nonempty.div_zero
added theorem Set.Nonempty.mul_zero
added theorem Set.Nonempty.zero_div
added theorem Set.Nonempty.zero_mul
added theorem Set.div_zero_subset
added theorem Set.mul_zero_subset
added theorem Set.zero_div_subset
added theorem Set.zero_mul_subset
added theorem Set.add_mul_subset
added theorem Set.mul_add_subset