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