Commit 2025-07-04 07:44 27a84eb7

View on Github →

chore: further whitespace fixes (#26708) Found by #26706: likely not exhaustive, but a good first approximation.

Estimated changes

modified theorem TopModuleCat.hom_ofHom
modified theorem toAdd_vadd
modified theorem toMul_smul
modified theorem Fin.insertNth_div
modified theorem Set.prod_mul_prod_comm
modified theorem WithZero.map'_map'
modified theorem ComplexShape.not_rel_of_eq
modified theorem SSet.horn.hom_ext
modified theorem AnalyticAt.fun_zpow
modified theorem AnalyticOn.zpow
modified theorem cfc_nnreal_eq_real
modified theorem cfc_real_eq_complex
modified theorem cfcₙ_nnreal_eq_real
modified theorem cfcₙ_real_eq_complex
modified theorem cfcₙ_comp_neg
modified theorem CFC.inv_nonneg
modified theorem cfc_comp_neg
modified theorem BitVec.toFin_nsmul
modified theorem BitVec.toFin_pow
modified theorem BitVec.toFin_zsmul
modified theorem Fin.add_rev_cast
modified theorem Fin.rev_add_cast
modified theorem Fin.orderSucc_last
modified theorem Subgroup.relindex_ne_zero
modified theorem FixedDetMatrices.ext
modified theorem Matrix.map_mul_intCast
modified theorem MultilinearMap.map_update
modified theorem Equiv.embeddingFinSucc_fst
modified theorem Equiv.embeddingFinSucc_snd
modified theorem Function.forall_update_iff
modified theorem Function.hfunext
modified theorem MeasureTheory.ae_eq_top
modified theorem Summable.clog_one_sub
modified theorem LTSeries.range_apply
modified theorem ContinuousMulEquiv.coe_mk'
modified theorem summable_partition
modified theorem RestrictedProduct.ext