Commit 2024-07-12 15:32 d419680b

View on Github →

chore: remove spaces in binders (#14664) These were found by the linter at #14379.

Estimated changes

Modified Mathlib/Algebra/RingQuot.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean

modified theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_hom

Modified Mathlib/CategoryTheory/Comma/Over.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

modified theorem MulActionHom.comp_inverse'

modified theorem MulActionHom.inverse'_comp

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

modified theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀

Modified Mathlib/Order/Hom/CompleteLattice.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

Modified test/congr.lean

Modified test/hint.lean