Commit 2025-08-11 12:31 4161fc53

View on Github →

chore: more indentation fixes (#28118) Found by the linter in #27996.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/Logic/Equiv/Sum.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/NumberTheory/LSeries/DirichletContinuation.lean

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/CompleteLattice/Basic.lean

Modified Mathlib/Order/Nucleus.lean

Modified Mathlib/Order/Radical.lean

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Independence/Integration.lean

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

modified theorem FractionalIdeal.num_eq_zero_iff

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

Modified Mathlib/RingTheory/QuotSMulTop.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

Modified Mathlib/RingTheory/Valuation/Extension.lean

Modified Mathlib/Tactic/CC/Lemmas.lean

Modified Mathlib/Tactic/Find.lean

Modified Mathlib/Tactic/FunProp/Types.lean

Modified Mathlib/Tactic/Linter/TextBased.lean

Modified Mathlib/Tactic/SplitIfs.lean

Modified Mathlib/Tactic/Widget/Conv.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

Modified Mathlib/Topology/Algebra/Module/WeakDual.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

Modified Mathlib/Topology/Spectral/Hom.lean

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean