Commit 2024-11-23 06:55 4b6c6f87

View on Github →

chore: cleanup of nolint simpNF (#19061)

Estimated changes

Modified Mathlib/Algebra/Algebra/Unitization.lean

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

added theorem Finsupp.if_mem_support

deleted theorem Finsupp.sum_ite_self_eq_aux

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

Modified Mathlib/Algebra/Homology/ShortComplex/Homology.lean

Modified Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

Modified Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

Modified Mathlib/Algebra/Lie/IdealOperations.lean

Modified Mathlib/Algebra/Module/GradedModule.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Ring/Semiconj.lean

modified theorem SemiconjBy.neg_one_left

modified theorem SemiconjBy.neg_one_right

Modified Mathlib/Algebra/Star/Subsemiring.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean