Commit 2025-03-20 15:13 bcaf02fa

chore(Algebra/Group/Pointwise/Finset): drop unnecessary import (#23148) The file Mathlib.Algebra.Group.Pointwise.Finset.Basic imported Mathlib.Algebra.Ring.Nat but it seems this import is actually unneeded. We can drop it and add the commented-out assert_not_exists MonoidWithZero. Spotted while looking at potential files to split.