Mathlib Changelog
v4
Changelog
About
Github
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