Commit 2023-09-13 13:29 7eb27432

View on Github →

chore: tidy various files (#7132)

Estimated changes

Modified Archive/Imo/Imo2008Q4.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Modified Mathlib/Algebra/Module/LocalizedModule.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

deleted theorem AlgebraicGeometry.QuasiCompact.affine_openCover_tFAE

added theorem AlgebraicGeometry.QuasiCompact.affine_openCover_tfae

deleted theorem AlgebraicGeometry.QuasiCompact.openCover_tFAE

added theorem AlgebraicGeometry.QuasiCompact.openCover_tfae

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Analysis/Convex/Normed.lean

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/CategoryTheory/Abelian/Pseudoelements.lean

Modified Mathlib/CategoryTheory/Bicategory/Adjunction.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/Data/Set/Card.lean

added theorem Set.Infinite.exists_superset_ncard_eq

deleted theorem Set.Infinite.exists_supset_ncard_eq

modified theorem Set.encard_eq_two

modified theorem Set.encard_pair

added theorem Set.exists_superset_subset_encard_eq

deleted theorem Set.exists_supset_subset_encard_eq

Modified Mathlib/Data/Set/Function.lean

deleted theorem Function.LeftInvOn_invFunOn_of_subset_image_image

added theorem Function.leftInvOn_invFunOn_of_subset_image_image

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean

modified theorem NumberField.Units.rootsOfUnity_eq_one

added def NumberField.Units.torsionOrder

deleted def NumberField.Units.torsion_order

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/Topology/PathConnected.lean