Theorem Dioph.of_no_dummies

Modification history

2026-05-08 23:32

Mathlib/NumberTheory/Dioph.lean

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

Modified Dioph.of_no_dummies View on Github →

2023-06-11 15:31

Mathlib/NumberTheory/Dioph.lean

feat: port NumberTheory.Dioph (#4914)

Added Dioph.of_no_dummies View on Github →