Commit 2025-07-25 19:00 658f961e

View on Github →

chore: fix indentation of subsequent declaration lines (#27478) Found by the linter in #27473; not exhaustive.

Estimated changes

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

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

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

modified def OneHom.inverse

Modified Mathlib/Algebra/GroupWithZero/Action/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Hom.lean

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

Modified Mathlib/Control/Basic.lean

Modified Mathlib/Data/List/Basic.lean

modified theorem List.left_le_of_mem_range'

modified theorem List.range'_0

Modified Mathlib/Data/List/TakeDrop.lean

Modified Mathlib/Data/Nat/Cast/Defs.lean

Modified Mathlib/Data/Prod/Basic.lean

Modified Mathlib/Data/Seq/Computation.lean

modified theorem Computation.liftRelAux_inl_inl

Modified Mathlib/Data/Stream/Init.lean

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Order/ULift.lean

modified theorem ULift.down_compare

Modified Mathlib/Tactic/MkIffOfInductiveProp.lean

Modified Mathlib/Tactic/Sat/FromLRAT.lean

Modified Mathlib/Tactic/Simps/Basic.lean