Commit 2023-05-09 06:29 66cb7cc4

View on Github →

chore: tidy various files (#3848)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean

Modified Mathlib/Algebra/Homology/Homotopy.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

modified def CategoryTheory.Subobject.existsPullbackAdj

deleted def CategoryTheory.Subobject.exists_

modified theorem CategoryTheory.Subobject.exists_iso_map

added def CategoryTheory.Subobject.«exists»

Modified Mathlib/CategoryTheory/Subobject/FactorThru.lean

added theorem CategoryTheory.Subobject.factorThru_ofLE

deleted theorem CategoryTheory.Subobject.factorThru_ofLe

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

added def CategoryTheory.MonoOver.botLE

deleted def CategoryTheory.MonoOver.botLe

added def CategoryTheory.MonoOver.infLELeft

added def CategoryTheory.MonoOver.infLERight

deleted def CategoryTheory.MonoOver.infLeLeft

deleted def CategoryTheory.MonoOver.infLeRight

added def CategoryTheory.MonoOver.topLEPullbackSelf

deleted def CategoryTheory.MonoOver.topLePullbackSelf

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

modified def CategoryTheory.MonoOver.existsIsoMap

modified def CategoryTheory.MonoOver.existsPullbackAdj

deleted def CategoryTheory.MonoOver.exists_

added def CategoryTheory.MonoOver.«exists»

Modified Mathlib/Data/Dfinsupp/Order.lean

modified def Dfinsupp.orderEmbeddingToFun

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.snoc_castSucc

deleted theorem Fin.snoc_cast_succ

added theorem Fin.snoc_comp_castSucc

deleted theorem Fin.snoc_comp_cast_succ

Modified Mathlib/Data/Nat/Cast/Defs.lean

Modified Mathlib/Data/Seq/WSeq.lean

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

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

added theorem MeasureTheory.nullMeasurableSet_toMeasurable

deleted theorem MeasureTheory.nullMeasurableSet_to_measurable

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

deleted theorem Ideal.comap_Inf'

added theorem Ideal.comap_infₛ'

modified def Ideal.relIsoOfBijective

modified def Ideal.relIsoOfSurjective

Modified Mathlib/Topology/Category/Top/Limits/Basic.lean

added def TopCat.initialIsoPEmpty

deleted def TopCat.initialIsoPempty

added def TopCat.isInitialPEmpty

deleted def TopCat.isInitialPempty

added def TopCat.isTerminalPUnit

deleted def TopCat.isTerminalPunit

added def TopCat.terminalIsoPUnit

deleted def TopCat.terminalIsoPunit

Modified Mathlib/Topology/Homotopy/Basic.lean

modified def ContinuousMap.Homotopy.symm

Modified Mathlib/Topology/Order/Basic.lean

deleted theorem Antitone.map_csupr_of_continuousAt

added theorem Antitone.map_csupᵢ_of_continuousAt

deleted theorem Monotone.map_csupr_of_continuousAt

added theorem Monotone.map_csupᵢ_of_continuousAt