Commit 2024-07-24 14:53 df91bcc8

View on Github →

fix: shorten lines with 101 characters (#15104) Found by the long line syntax linter at #15097.

Estimated changes

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

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

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

modified theorem AlgebraicGeometry.Scheme.toΓSpec_image_zeroLocus_eq_of_isAffine

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

Modified Mathlib/Analysis/NormedSpace/WeakOperatorTopology.lean

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

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/Monad/Equalizer.lean

modified def CategoryTheory.Comonad.CofreeEqualizer.bottomMap

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Data/Finset/SMulAntidiagonal.lean

modified theorem Set.IsPWO.smul

Modified Mathlib/Data/Matroid/Map.lean

Modified Mathlib/FieldTheory/Galois.lean

modified theorem IsGalois.tfae

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

modified theorem AffineEquiv.injective_pointReflection_left_of_injective_bit0

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

Modified Mathlib/MeasureTheory/Function/Intersectivity.lean

Modified Mathlib/MeasureTheory/Order/UpperLower.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean

Modified Mathlib/RingTheory/AlgebraTower.lean

added def Basis.smulTower

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

Modified Mathlib/RingTheory/WittVector/Frobenius.lean

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean

Modified Mathlib/Topology/Homotopy/Product.lean