Commit 2024-08-16 13:44 4ecf8823

View on Github →

chore: fix some to_additive technical debt (#15852)

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Group/InjSurj.lean

Modified Mathlib/Algebra/Group/Opposite.lean

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

Modified Mathlib/Algebra/Order/Group/Synonym.lean

Modified Mathlib/Algebra/Order/Hom/Basic.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

Modified Mathlib/Combinatorics/Additive/RuzsaCovering.lean

Modified Mathlib/Data/Finset/Pointwise/Basic.lean

Modified Mathlib/Data/Set/Pointwise/Basic.lean

deleted theorem Set.nsmul_univ

Modified Mathlib/Logic/Small/Group.lean

deleted theorem equivShrink_add

deleted theorem equivShrink_neg

deleted theorem equivShrink_sub

deleted theorem equivShrink_symm_add

deleted theorem equivShrink_symm_neg

deleted theorem equivShrink_symm_sub

deleted theorem equivShrink_symm_zero

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

Modified Mathlib/Topology/Support.lean

Modified scripts/style-exceptions.txt