Commit 2023-04-17 14:24 dcd5622e

View on Github →

chore: tidy various files (#3483)

Estimated changes

Modified Mathlib/Algebra/Order/Nonneg/Ring.lean

modified theorem Nonneg.toNonneg_lt

Modified Mathlib/CategoryTheory/Arrow.lean

added theorem CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right

deleted theorem CategoryTheory.Arrow.isIso_of_iso_left_of_isIso_right

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

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

modified def CategoryTheory.Limits.Cofork.ofπ

modified def CategoryTheory.Limits.Fork.ofι

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

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

added def MeasurableEquiv.piMeasurableEquivTProd

deleted def MeasurableEquiv.piMeasurableEquivTprod

added theorem measurable_findGreatest'

deleted theorem measurable_find_greatest'

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.mk_pEmpty

deleted theorem Cardinal.mk_pLift_false

deleted theorem Cardinal.mk_pLift_true

deleted theorem Cardinal.mk_pSum

deleted theorem Cardinal.mk_pUnit

added theorem Cardinal.mk_pempty

added theorem Cardinal.mk_plift_false

added theorem Cardinal.mk_plift_true

added theorem Cardinal.mk_psum

added theorem Cardinal.mk_punit

modified def Cardinal.toPartENat

Modified Mathlib/SetTheory/Cardinal/Finite.lean

deleted theorem Nat.card_pLift

added theorem Nat.card_plift

deleted theorem Nat.card_uLift

added theorem Nat.card_ulift

deleted theorem Nat.card_zMod

added theorem Nat.card_zmod