Commit 2023-02-22 19:59 54bf6e04

View on Github →

chore: tidy various files (#2446)

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem algebraMap.coe_ratCast

deleted theorem algebraMap.coe_rat_cast

added theorem intCast_smul

deleted theorem int_cast_smul

Modified Mathlib/CategoryTheory/Arrow.lean

modified def CategoryTheory.Functor.mapArrow

Modified Mathlib/CategoryTheory/Category/Preorder.lean

modified theorem CategoryTheory.homOfLE_leOfHom

Modified Mathlib/CategoryTheory/Core.lean

Modified Mathlib/CategoryTheory/IsomorphismClasses.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean

Modified Mathlib/Data/Bool/Basic.lean

Modified Mathlib/Data/PFunctor/Univariate/M.lean

Modified Mathlib/Deprecated/Subring.lean

Modified Mathlib/Order/PFilter.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/Completion.lean

deleted theorem CauchyFilter.cauchyCat_eq

added theorem CauchyFilter.cauchyFilter_eq

deleted theorem CauchyFilter.nonempty_cauchyCat_iff

added theorem CauchyFilter.nonempty_cauchyFilter_iff

modified def UniformSpace.Completion.cPkg