Commit 2024-06-09 16:47 afbd7e51

View on Github →

chore: remove some set_option ... in which are not necessary any more (#13655) All of them are related backwards compatibility flags. Found by adomani's linter in #13653, not exhaustive.

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Homology/Exact.lean

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

Modified Mathlib/Analysis/Convex/Slope.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

Modified Mathlib/GroupTheory/CommutingProbability.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

Modified Mathlib/LinearAlgebra/QuotientPi.lean

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/Topology/Order/IntermediateValue.lean