Commit 2023-06-13 06:07 95de1dee

View on Github →

chore: tidy various files (#4997)

Estimated changes

Modified Mathlib/Algebra/Order/CompleteField.lean

modified def LinearOrderedField.inducedAddHom

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean

Modified Mathlib/CategoryTheory/Closed/Zero.lean

added def CategoryTheory.equivPUnit

deleted def CategoryTheory.equivPunit

Modified Mathlib/CategoryTheory/IsConnected.lean

added def CategoryTheory.discreteIsConnectedEquivPUnit

deleted def CategoryTheory.discreteIsConnectedEquivPunit

Modified Mathlib/CategoryTheory/Limits/Comma.lean

Modified Mathlib/CategoryTheory/Limits/Unit.lean

deleted def CategoryTheory.Limits.pUnitCocone

deleted def CategoryTheory.Limits.pUnitCoconeIsColimit

deleted def CategoryTheory.Limits.pUnitCone

deleted def CategoryTheory.Limits.pUnitConeIsLimit

added def CategoryTheory.Limits.punitCocone

added def CategoryTheory.Limits.punitCoconeIsColimit

added def CategoryTheory.Limits.punitCone

added def CategoryTheory.Limits.punitConeIsLimit

Modified Mathlib/CategoryTheory/PUnit.lean

deleted def CategoryTheory.Functor.pUnitExt

deleted theorem CategoryTheory.Functor.pUnit_ext'

added def CategoryTheory.Functor.punitExt

added theorem CategoryTheory.Functor.punit_ext'

deleted theorem CategoryTheory.equiv_pUnit_iff_unique

added theorem CategoryTheory.equiv_punit_iff_unique

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem IsAlgClosed.algebraMap_surjective_of_isIntegral'

deleted theorem IsAlgClosed.algebra_map_surjective_of_is_integral'

Modified Mathlib/Probability/Integration.lean

Modified Mathlib/RingTheory/ClassGroup.lean

Modified Mathlib/RingTheory/DedekindDomain/Dvr.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean