Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-12 08:26
5a23b873
View on Github →
chore(whitespace): changing yet more spaces (
#22858
) Found by
#22760
.
Estimated changes
Modified
Mathlib/Algebra/Homology/HomologySequence.lean
Modified
Mathlib/Algebra/Homology/Linear.lean
Modified
Mathlib/Algebra/QuaternionBasis.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
modified
theorem
SSet.StrictSegal.spineToSimplex_interval
Modified
Mathlib/Analysis/Asymptotics/TVS.lean
Modified
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
Modified
Mathlib/Analysis/LocallyConvex/Barrelled.lean
Modified
Mathlib/Analysis/NormedSpace/OperatorNorm/Asymptotics.lean
Modified
Mathlib/Data/Bundle.lean
Modified
Mathlib/FieldTheory/Minpoly/Field.lean
modified
theorem
minpoly.eq_iff_aeval_eq_zero
Modified
Mathlib/FieldTheory/Perfect.lean
modified
theorem
iterateFrobeniusEquiv_zero
Modified
Mathlib/GroupTheory/Coxeter/Inversion.lean
modified
theorem
CoxeterSystem.IsReflection.not_isLeftInversion_mul_right_iff
Modified
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Basic.lean
Modified
Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
Modified
Mathlib/RingTheory/Adjoin/Field.lean
Modified
Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
Modified
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
modified
theorem
HasProd.sigma_of_hasProd
modified
theorem
Multipliable.sigma'
modified
theorem
Multipliable.sigma
modified
theorem
Multipliable.sigma_factor
modified
theorem
tprod_sigma'
modified
theorem
tprod_sigma
Modified
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
modified
theorem
HasSum.const_div
Modified
Mathlib/Topology/Algebra/OpenSubgroup.lean
modified
theorem
Subgroup.isOpen_of_openSubgroup
Modified
Mathlib/Topology/Instances/ENNReal/Lemmas.lean
Modified
Mathlib/Topology/Instances/Matrix.lean
modified
theorem
Continuous.matrix_blockDiag'
modified
theorem
HasSum.matrix_blockDiag'
modified
theorem
Summable.matrix_blockDiag'
Modified
Mathlib/Topology/MetricSpace/Gluing.lean
modified
theorem
Metric.Sigma.fst_eq_of_dist_lt_one
modified
def
Metric.Sigma.instDist