Commit 2025-07-09 14:52 a38eeafd

View on Github →

chore: space following Σ (#26932) Found by #26926. These are just changes to Σ/Σ' not followed by a space that add a space.

Estimated changes

modified def DirectSum.sigmaLcurry
modified def Finset.symInsertEquiv
modified def List.equivSigmaTuple
modified theorem Multiset.mem_sigma
modified def PFun.equivSubtype
modified theorem Set.Sigma.univ
modified theorem Set.iUnion_eq_range_psigma
modified theorem Set.iUnion_eq_range_sigma
modified def Prod.toSigma
modified theorem Sigma.eta
modified def WType.equivSigma
modified def WType.ofSigma
modified def WType.toSigma
modified theorem WType.toSigma_ofSigma
modified def upperCentralSeriesAux
modified def Equiv.Perm.finPairsLT
modified def Equiv.Perm.signBijAux
modified def TopCat.sigmaIsoSigma
modified theorem Metric.Sigma.isometry_mk