Commit 2025-08-02 11:30 359a2a60

View on Github →

chore: various indentation fixes (#27869) Found by the linter in #27525.

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

modified theorem LieAlgebra.IsKilling.eq_top_of_invtSubmodule_ne_bot

Modified Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/Analysis/InnerProductSpace/Harmonic/Constructions.lean

modified theorem AnalyticAt.harmonicAt_conj

Modified Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Basic.lean

Modified Mathlib/CategoryTheory/GradedObject/Trifunctor.lean

Modified Mathlib/CategoryTheory/Join/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Localization/Trifunctor.lean

Modified Mathlib/CategoryTheory/Shift/Localization.lean

Modified Mathlib/CategoryTheory/Shift/SingleFunctors.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/FieldTheory/JacobsonNoether.lean

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

Modified Mathlib/MeasureTheory/SetSemiring.lean

Modified Mathlib/ModelTheory/Basic.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

Modified Mathlib/RingTheory/Frobenius.lean

Modified Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean

Modified Mathlib/RingTheory/Unramified/Finite.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

Modified Mathlib/Tactic/Widget/SelectPanelUtils.lean

Modified Mathlib/Topology/Algebra/ProperAction/Basic.lean

Modified Mathlib/Topology/GDelta/Basic.lean

modified theorem isMeagre_iUnion