Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
ADE_inequality.admissible_of_one_lt_sum_inv_aux
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.admissible_of_one_lt_sum_inv_aux
View on Github →