Commit 2023-04-07 15:31 dc65937e

View on Github →

feat(number_theory/pell): add API for solutions (#18626) This continues the devlopment of the theory of Pell's equation. We add some API lemmas for solutions, which will be needed for defining of the fundamental solution and proving its properties. See this Zulip thread.

Estimated changes

Modified src/number_theory/pell.lean

deleted theorem pell.exists_pos_of_not_is_square

added theorem pell.solution₁.eq_one_of_x_eq_one

added theorem pell.solution₁.eq_one_or_neg_one_iff_y_eq_zero

added theorem pell.solution₁.eq_zero_of_d_neg

added theorem pell.solution₁.exists_nontrivial_of_not_is_square

added theorem pell.solution₁.exists_pos_of_not_is_square

added theorem pell.solution₁.exists_pos_variant

added theorem pell.solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos

added theorem pell.solution₁.x_mul_pos

added theorem pell.solution₁.x_ne_zero

added theorem pell.solution₁.x_pow_pos

added theorem pell.solution₁.x_zpow_pos

added theorem pell.solution₁.y_mul_pos

added theorem pell.solution₁.y_ne_zero_of_one_lt_x

added theorem pell.solution₁.y_pow_succ_pos