Mathlib v3 is deprecated. Go to Mathlib v4

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)

Estimated changes

Created src/number_theory/ADE_inequality.lean

added def ADE_inequality.A'

added def ADE_inequality.A

added def ADE_inequality.D'

added def ADE_inequality.E'

added def ADE_inequality.E6

added def ADE_inequality.E7

added def ADE_inequality.E8

added theorem ADE_inequality.admissible.one_lt_sum_inv

added def ADE_inequality.admissible

added theorem ADE_inequality.admissible_A'

added theorem ADE_inequality.admissible_D'

added theorem ADE_inequality.admissible_E'3

added theorem ADE_inequality.admissible_E'4

added theorem ADE_inequality.admissible_E'5

added theorem ADE_inequality.admissible_E6

added theorem ADE_inequality.admissible_E7

added theorem ADE_inequality.admissible_E8

added theorem ADE_inequality.admissible_of_one_lt_sum_inv

added theorem ADE_inequality.admissible_of_one_lt_sum_inv_aux'

added theorem ADE_inequality.admissible_of_one_lt_sum_inv_aux

added theorem ADE_inequality.classification

added theorem ADE_inequality.lt_four

added theorem ADE_inequality.lt_six

added theorem ADE_inequality.lt_three

added def ADE_inequality.sum_inv

added theorem ADE_inequality.sum_inv_pqr