Commit 2023-05-30 06:01 4acdb595

View on Github →

feat: port Data.Real.GoldenRatio (#4332)

Estimated changes

added theorem Real.coe_fib_eq'
added theorem Real.coe_fib_eq
added def fibRec
added theorem fibRec_charPoly_eq
added theorem fib_isSol_fibRec
added theorem geom_gold_isSol_fibRec
added theorem goldConj_irrational
added theorem goldConj_mul_gold
added theorem goldConj_ne_zero
added theorem goldConj_neg
added theorem goldConj_sq
added theorem gold_add_goldConj
added theorem gold_irrational
added theorem gold_mul_goldConj
added theorem gold_ne_zero
added theorem gold_pos
added theorem gold_sq
added theorem gold_sub_goldConj
added def goldenConj
added def goldenRatio
added theorem inv_gold
added theorem inv_goldConj
added theorem neg_one_lt_goldConj
added theorem one_lt_gold
added theorem one_sub_gold
added theorem one_sub_goldConj