Commit 2023-04-24 05:58 e3fe5faf

View on Github →

chore: tidy various files (#3606)

Estimated changes

Modified Mathlib/Algebra/Homology/Exact.lean

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

deleted theorem tFAE_memIooMod

added theorem tfae_memIooMod

Modified Mathlib/Analysis/Normed/Group/AddTorsor.lean

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

Modified Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem closedUnderRestriction'

deleted theorem closed_under_restriction'

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

deleted theorem Valuation.IsEquiv_iff_val_eq_one

deleted theorem Valuation.IsEquiv_iff_val_le_one

deleted theorem Valuation.IsEquiv_iff_val_lt_one

deleted theorem Valuation.IsEquiv_iff_val_sub_one_lt_one

deleted theorem Valuation.IsEquiv_of_map_strictMono

deleted theorem Valuation.IsEquiv_of_val_le_one

deleted theorem Valuation.IsEquiv_tFAE

added theorem Valuation.isEquiv_iff_val_eq_one

added theorem Valuation.isEquiv_iff_val_le_one

added theorem Valuation.isEquiv_iff_val_lt_one

added theorem Valuation.isEquiv_iff_val_sub_one_lt_one

added theorem Valuation.isEquiv_of_map_strictMono

added theorem Valuation.isEquiv_of_val_le_one

added theorem Valuation.isEquiv_tfae

Modified Mathlib/Topology/MetricSpace/Closeds.lean