Def ADE_inequality.A

Modification history

2021-02-13 00:49

src/number_theory/ADE_inequality.lean

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

Added ADE_inequality.A View on Github →