Commit 2024-09-12 22:13 56da879c

View on Github →

chore: Move pointwise finset lemmas under Algebra (#16744)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Renamed Mathlib/Data/Finset/Pointwise/Basic.lean to Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

Renamed Mathlib/Data/Finset/Pointwise/Interval.lean to Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean

Renamed Mathlib/Data/Finset/Pointwise/Card.lean to Mathlib/Algebra/Group/Pointwise/Finset/NatCard.lean

Modified Mathlib/Algebra/Group/UniqueProds/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

Modified Mathlib/Algebra/Order/Antidiag/Pi.lean

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

Modified Mathlib/Combinatorics/Additive/ETransform.lean

Modified Mathlib/Combinatorics/Additive/Energy.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Combinatorics/Additive/RuzsaCovering.lean

Modified Mathlib/Data/DFinsupp/Interval.lean

Modified Mathlib/Data/Finset/Finsupp.lean

Modified Mathlib/Data/Finset/NatDivisors.lean