Commit 2026-05-08 23:32 043e9e04

View on Github →

chore(NumberTheory/Dioph): reduce defeq abuse of Set α = α → Prop (#39099)

Estimated changes

modified theorem Dioph.diophPFun_vec
modified theorem Dioph.dioph_comp2
modified theorem Dioph.dvd_dioph
modified theorem Dioph.eq_dioph
modified theorem Dioph.modEq_dioph
modified theorem Dioph.of_no_dummies