# Commit 2021-02-13 00:49 e79bf053

View on Github →feat(number_theory/ADE_inequality): the inequality 1/p + 1/q + 1/r > 1 (#6156)

Mathlib v3 is deprecated. Go to Mathlib v4

feat(number_theory/ADE_inequality): the inequality 1/p + 1/q + 1/r > 1 (#6156)