Commit 2025-03-12 09:09 0edea251

View on Github →

chore(whitespace): some more changes in whitespace (#22840) Found by #22760.

Estimated changes

Modified Mathlib/Algebra/Central/Basic.lean

Modified Mathlib/Algebra/Group/Action/Equidecomp.lean

Modified Mathlib/Algebra/Group/Submonoid/Units.lean

Modified Mathlib/Algebra/Module/LinearMap/Basic.lean

modified theorem DomMulAct.coe_smul_linearMap

Modified Mathlib/Algebra/Quaternion.lean

modified theorem QuaternionAlgebra.equivTuple_apply

Modified Mathlib/CategoryTheory/Limits/Final.lean

modified theorem CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel

Modified Mathlib/Data/Seq/Seq.lean

modified theorem Stream'.Seq.terminates_map_iff

Modified Mathlib/LinearAlgebra/Vandermonde.lean

modified theorem Matrix.projVandermonde_apply_of_ne_zero

modified theorem Matrix.projVandermonde_apply_zero_right

Modified Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean

modified theorem MeasureTheory.measure_liminf_cofinite_eq_zero

Modified Mathlib/RingTheory/Finiteness/Subalgebra.lean

modified theorem Subalgebra.fg_bot_toSubmodule

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

modified theorem MvPolynomial.homogeneousComponent_mem

Modified Mathlib/SetTheory/Cardinal/Regular.lean

modified theorem Cardinal.IsInaccessible.mk