Commit 2025-03-10 21:18 89df859f

View on Github →

chore: more whitespace adaptation (#22785) Found by #22760.

Estimated changes

Modified Mathlib/Algebra/Star/StarRingHom.lean

modified theorem StarRingEquiv.symm_trans_apply

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.castPred_zero

Modified Mathlib/Data/List/Basic.lean

modified theorem List.getLast?_flatten_replicate

Modified Mathlib/Data/List/Nodup.lean

modified theorem List.Nodup.sigma

Modified Mathlib/Tactic/CategoryTheory/Reassoc.lean

Modified Mathlib/Tactic/NormNum/Pow.lean