Commit 2024-06-06 16:20 cc4f9966

View on Github →

chore: tidy various files (#13562)

Estimated changes

Modified Mathlib/Algebra/DirectLimit.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

Modified Mathlib/Algebra/MonoidAlgebra/Ideal.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

modified theorem CategoryTheory.IsPreconnected.of_any_functor_const_on_obj

Modified Mathlib/CategoryTheory/Localization/Triangulated.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Prod/Lex.lean

Modified Mathlib/GroupTheory/GroupAction/Opposite.lean

Modified Mathlib/GroupTheory/NoncommCoprod.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/CategoryTheory.lean

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Integral/Pi.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/Order/Partition/Equipartition.lean

Modified Mathlib/Order/RelSeries.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/FiniteType.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

Modified Mathlib/Topology/Algebra/UniformMulAction.lean

Modified Mathlib/Topology/Homotopy/HSpaces.lean