Commit 2025-10-19 14:27 aa7a3d97

View on Github →

chore: miscellaneous linter whitespace fixes (#30663) Extracted from #30658. Found by adomani's extension of the commandStart linter to proof bodies.

Estimated changes

modified theorem CharP.cast_eq_iff_mod_eq
modified theorem npow_add
modified theorem WithZero.exp_neg
modified theorem WithZero.exp_sub
modified theorem StarMonoidHom.coe_mk
modified theorem NonUnitalStarRingHom.coe_mk
modified theorem BitVec.ofFin_intCast
modified theorem Bool.toNat_beq_one
modified theorem Bool.toNat_bne_zero
modified theorem DFinsupp.toMultiset_sup
modified theorem Nat.coprime_of_lt_minFac
modified theorem MultilinearMap.coe_smul