Commit 2025-05-14 07:02 6534503f

View on Github →

chore: fix some indentation (#24874)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

Modified Mathlib/Deprecated/Cardinal/Finite.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/Logic/Relation.lean