Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-22 00:21 278f5120

View on Github →

feat(data/real): define the golden ratio and its conjugate, prove irrationality of both and Binet's formula (#3885) Co-authored by @alreadydone and @monadius through their solutions to the corresponding Codewars Kata.

Estimated changes

added theorem fib_is_sol_fib_rec
added def fib_rec
added theorem fib_rec_char_poly_eq
added theorem gold_add_gold_conj
added theorem gold_conj_irrational
added theorem gold_conj_mul_gold
added theorem gold_conj_ne_zero
added theorem gold_conj_neg
added theorem gold_conj_sq
added theorem gold_irrational
added theorem gold_mul_gold_conj
added theorem gold_ne_zero
added theorem gold_pos
added theorem gold_sq
added theorem gold_sub_gold_conj
added def golden_conj
added def golden_ratio
added theorem inv_gold
added theorem inv_gold_conj
added theorem neg_one_lt_gold_conj
added theorem one_lt_gold
added theorem one_sub_gold
added theorem one_sub_gold_conj
added theorem real.coe_fib_eq'
added theorem real.coe_fib_eq