Commit 2025-03-12 09:09 8ab42a61

View on Github →

chore(whitespace): lots of whitespace (#22838) Found by #22760.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

modified theorem DirectSum.sigmaLcurry_apply

Modified Mathlib/Algebra/Order/Ring/Cast.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Modified Mathlib/Algebra/Ring/Rat.lean

Modified Mathlib/CategoryTheory/Abelian/Exact.lean

modified theorem CategoryTheory.Abelian.tfae_epi

Modified Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

modified theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom

Modified Mathlib/Data/Finsupp/Basic.lean

modified theorem Finsupp.sigmaFinsuppEquivPiFinsupp_apply

modified theorem Finsupp.sigma_sum

Modified Mathlib/Data/Finsupp/ToDFinsupp.lean

modified def sigmaFinsuppAddEquivDFinsupp

modified def sigmaFinsuppEquivDFinsupp

modified theorem sigmaFinsuppEquivDFinsupp_add

modified theorem sigmaFinsuppEquivDFinsupp_apply

modified theorem sigmaFinsuppEquivDFinsupp_single

modified theorem sigmaFinsuppEquivDFinsupp_symm_apply

Modified Mathlib/Data/Matrix/Block.lean

modified def Matrix.blockDiag'

modified theorem Matrix.blockDiag'_add

modified theorem Matrix.blockDiag'_apply

modified theorem Matrix.blockDiag'_diagonal

modified theorem Matrix.blockDiag'_map

modified theorem Matrix.blockDiag'_neg

modified theorem Matrix.blockDiag'_sub

modified theorem Matrix.blockDiag'_transpose

modified theorem Matrix.blockDiag'_zero

modified def Matrix.blockDiagonal'

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

modified theorem Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

modified theorem LinearMap.add_compAlternatingMap

modified theorem LinearMap.zero_compAlternatingMap

Modified Mathlib/LinearAlgebra/Finsupp/SumProd.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

modified theorem LinearMap.add_compMultilinearMap

modified theorem LinearMap.zero_compMultilinearMap

Modified Mathlib/Order/Filter/Cocardinal.lean

modified theorem Filter.eventually_cocardinal_nmem_of_card_lt

Modified Mathlib/Order/Fin/Basic.lean

Modified Mathlib/Probability/Independence/Kernel.lean

Modified Mathlib/Probability/Kernel/Defs.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

modified theorem Ideal.add_pow_add_pred_mem_of_pow_mem

modified theorem Ideal.add_pow_add_pred_mem_of_pow_mem_of_commute

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Ideal.sup_multiset_prod_eq_top

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Nilpotent/Exp.lean

modified theorem IsNilpotent.exp_eq_truncated

Modified Mathlib/RingTheory/PowerSeries/Trunc.lean

modified theorem PowerSeries.trunc_mul_trunc

modified theorem PowerSeries.trunc_trunc_mul

Modified Mathlib/RingTheory/Valuation/ValExtension.lean

modified theorem IsValExtension.instIsLocalHomValuationInteger

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Game/Birthday.lean

modified theorem SetTheory.Game.birthday_quot_le_pGameBirthday

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Enum.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

Modified Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean

Modified Mathlib/Tactic/Module.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

modified theorem Profinite.NobelingProof.Products.prop_of_isGood_of_contained

Modified Mathlib/Topology/Connected/Clopen.lean

modified theorem Sigma.isConnected_iff

Modified Mathlib/Topology/Order/ScottTopology.lean

Modified Mathlib/Topology/PreorderRestrict.lean