Commit 2024-11-23 07:36 dde4596f

View on Github →

chore: cleanup of many set_option deprecated.linter false (#19181)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/AddTorsor.lean

deleted theorem Equiv.injective_pointReflection_left_of_injective_bit0

added theorem Equiv.injective_pointReflection_left_of_injective_two_nsmul

deleted theorem Equiv.pointReflection_fixed_iff_of_injective_bit0

added theorem Equiv.pointReflection_fixed_iff_of_injective_two_nsmul

Modified Mathlib/Algebra/BigOperators/Group/List.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

modified theorem div_mul_right

Modified Mathlib/Algebra/Ring/Parity.lean

Modified Mathlib/Data/FP/Basic.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Nat/Defs.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Num/Prime.lean

Renamed Mathlib/Data/LazyList/Basic.lean to Mathlib/Deprecated/LazyList.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

deleted theorem AffineEquiv.injective_pointReflection_left_of_injective_bit0

added theorem AffineEquiv.injective_pointReflection_left_of_injective_two_nsmul

deleted theorem AffineEquiv.pointReflection_fixed_iff_of_injective_bit0

added theorem AffineEquiv.pointReflection_fixed_iff_of_injective_two_nsmul

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Equiv/Nat.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/ModelTheory/Encoding.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified scripts/noshake.json