Commit 2023-08-01 09:41 865bd5b5

View on Github →

chore: cleanup some set_option commands (#6281)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Stirling.lean

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Modified Mathlib/Data/Nat/Factors.lean

Modified Mathlib/SetTheory/Game/PGame.lean

Modified Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

modified theorem SkyscraperPresheafFunctor.map'_id

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean