Commit 2023-09-22 11:29 11dbfb2b

View on Github →

chore: exactly 4 spaces in subsequent lines for def (#7321)

Estimated changes

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

Modified Mathlib/Algebra/Hom/Group/Defs.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

modified def HomologicalComplex.XIsoOfEq

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

Modified Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Algebra/Ring/Opposite.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

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

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

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean

Modified Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

modified def CategoryTheory.EffectiveEpi.getStruct

Modified Mathlib/Data/BinaryHeap.lean

Modified Mathlib/Data/Equiv/Functor.lean

Modified Mathlib/Data/TypeVec.lean

Modified Mathlib/Data/UnionFind.lean

Modified Mathlib/Lean/Expr/Basic.lean

Modified Mathlib/Lean/Meta/Simp.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

Modified Mathlib/Logic/Equiv/Functor.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

Modified Mathlib/Tactic/CasesM.lean

Modified Mathlib/Tactic/Choose.lean

Modified Mathlib/Tactic/Core.lean

Modified Mathlib/Tactic/MkIffOfInductiveProp.lean

Modified Mathlib/Tactic/PrintPrefix.lean

Modified Mathlib/Tactic/Ring/Basic.lean

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Testing/SlimCheck/Testable.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

modified def TopCat.piIsoPi

Modified Mathlib/Topology/Sheaves/Presheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean

Modified Mathlib/Topology/Specialization.lean

Modified test/Simps.lean

modified def AddHomPlus2.Simps.mul