Commit 2026-01-30 14:51 22559134
View on Github →chore: rename not_IntegrableOn_Ici_inv and not_IntegrableOn_Ioi_inv (#34613) Per rule 6 of the naming convention, they should be called not_integrableOn_Ici_inv resp. not_integrableOn_Ioi_inv.
chore: rename not_IntegrableOn_Ici_inv and not_IntegrableOn_Ioi_inv (#34613) Per rule 6 of the naming convention, they should be called not_integrableOn_Ici_inv resp. not_integrableOn_Ioi_inv.