Commit 2023-11-07 20:49 c97b9b00

View on Github →

fix: fixes of 3 PRs (#8248) Fixes mistake introduced in #7976 (ping to @alreadydone that you should use @[to_additive (attr := simp)] and not @[to_additive, simp]) and some namespacing mistakes from my own PRs #7337 and #7755

Estimated changes

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

Modified Mathlib/Algebra/Order/Monoid/Defs.lean

Modified Mathlib/Data/Fintype/Card.lean

added theorem Finset.card_add_card_compl

added theorem Finset.card_compl_add_card

deleted theorem card_add_card_compl

deleted theorem card_compl_add_card

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

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

added theorem HasCompactSupport.integral_Iic_deriv_eq

added theorem HasCompactSupport.integral_Ioi_deriv_eq

deleted theorem MeasureTheory.HasCompactSupport.integral_Iic_deriv_eq

deleted theorem MeasureTheory.HasCompactSupport.integral_Ioi_deriv_eq

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean