Commit 2025-08-24 19:45 6100c331

View on Github →

chore(Data/Real/GoldenRatio): namespace, fix names (#28815) The defs are called goldenRatio/goldenConj but were confusingly referred to as gold/goldConj in all lemma names.

Estimated changes

modified theorem Real.coe_fib_eq'
modified theorem Real.coe_fib_eq
added def Real.fibRec
added theorem Real.fib_isSol_fibRec
added theorem Real.goldenConj_neg
added theorem Real.goldenConj_sq
added theorem Real.goldenRatio_pos
added theorem Real.goldenRatio_sq
added theorem Real.inv_goldenConj
added theorem Real.inv_goldenRatio
deleted def fibRec
deleted theorem fibRec_charPoly_eq
deleted theorem fib_golden_conj_exp
deleted theorem fib_golden_exp'
deleted theorem fib_isSol_fibRec
deleted theorem geom_gold_isSol_fibRec
deleted theorem goldConj_irrational
deleted theorem goldConj_mul_gold
deleted theorem goldConj_ne_zero
deleted theorem goldConj_neg
deleted theorem goldConj_sq
deleted theorem gold_add_goldConj
deleted theorem gold_irrational
deleted theorem gold_lt_two
deleted theorem gold_mul_goldConj
deleted theorem gold_ne_zero
deleted theorem gold_pos
deleted theorem gold_pow_sub_gold_pow
deleted theorem gold_sq
deleted theorem gold_sub_goldConj
deleted theorem inv_gold
deleted theorem inv_goldConj
deleted theorem neg_one_lt_goldConj
deleted theorem one_lt_gold
deleted theorem one_sub_gold
deleted theorem one_sub_goldConj