Commit 2024-07-22 19:50 93c07b28

View on Github →

chore: robustifying for debug.byAsSorry (#14993) These are some minor changes, which are think are positive or neutral in any case, that help Mathlib compile under set_option debug.byAsSorry true (an option that arrived in v4.10 that turns all by blocks into sorries

Estimated changes

modified theorem IsUnit.dvd
modified theorem IsUnit.dvd_mul_left
modified theorem IsUnit.dvd_mul_right
modified theorem IsUnit.isPrimal
modified theorem IsUnit.mul_left_dvd
modified theorem IsUnit.mul_right_dvd
modified theorem List.foldl1_eq_foldr1
modified theorem List.foldl_eq_foldr
modified theorem List.getElem_indexOf
modified theorem List.getElem_ofFn_go
modified theorem MulHom.comp_noncommCoprod
modified def MulHom.noncommCoprod
modified theorem GaloisConnection.l_iSup
modified theorem GaloisConnection.l_iSup₂
modified theorem GaloisConnection.l_sSup
modified theorem GaloisConnection.u_eq