Commit 2025-04-30 07:12 0bdb916d

View on Github →

chore: whitespace adaptations (#24459) Found by a newer version of a whitespace linter, with a prototype at #24465.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

Modified Mathlib/Algebra/Star/StarRingHom.lean

modified def StarRingEquiv.trans

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

modified def CategoryTheory.MonoidalCategory.Pentagon

Modified Mathlib/Data/Fin/Tuple/Basic.lean

modified theorem Fin.sigma_eq_iff_eq_comp_cast

Modified Mathlib/Data/Int/LeastGreatest.lean

Modified Mathlib/Data/Vector/Basic.lean

modified def List.Vector.casesOn₂

modified def List.Vector.casesOn₃

Modified Mathlib/GroupTheory/Coset/Defs.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Modified Mathlib/Order/Fin/Finset.lean

Modified Mathlib/Probability/ConditionalProbability.lean

modified theorem ProbabilityTheory.inter_pos_of_cond_ne_zero

Modified Mathlib/Tactic/Abel.lean

Modified Mathlib/Tactic/FieldSimp.lean

Modified Mathlib/Tactic/Positivity/Basic.lean