GoldenRatio

📁 Source: Mathlib/NumberTheory/Real/GoldenRatio.lean

Statistics

Metric	Count
Definitions fibRec, goldenConj, goldenRatio, termφ, termψ	5
Theorems coe_fib_eq, coe_fib_eq', coe_intFib_eq, fibRec_charPoly_eq, fib_isSol_fibRec, fib_succ_sub_goldenConj_mul_fib, fib_succ_sub_goldenRatio_mul_fib, geom_goldConj_isSol_fibRec, geom_goldenConj_isSol_fibRec, geom_goldenRatio_isSol_fibRec, gold_pow_sub_gold_pow, goldenConj_irrational, goldenConj_mul_fib_succ_add_fib, goldenConj_mul_goldenRatio, goldenConj_ne_zero, goldenConj_neg, goldenConj_sq, goldenRatio_add_goldenConj, goldenRatio_irrational, goldenRatio_lt_two, goldenRatio_mul_fib_succ_add_fib, goldenRatio_mul_goldenConj, goldenRatio_ne_zero, goldenRatio_pos, goldenRatio_pow_sub_goldenRatio_pow, goldenRatio_sq, goldenRatio_sub_goldenConj, inv_goldenConj, inv_goldenRatio, neg_one_lt_goldenConj, one_lt_goldenRatio, one_sub_goldenConj, one_sub_goldenRatio, fib_golden_conj_exp, fib_golden_exp', geom_gold_isSol_fibRec, goldConj_irrational, goldConj_mul_gold, goldConj_ne_zero, goldConj_neg, goldConj_sq, gold_add_goldConj, gold_irrational, gold_lt_two, gold_mul_goldConj, gold_ne_zero, gold_pos, gold_sq, gold_sub_goldConj, inv_gold, inv_goldConj, neg_one_lt_goldConj, one_lt_gold, one_sub_gold, one_sub_goldConj	55
Total	60

Real

Definitions

Name	Category	Theorems
fibRec 📖	CompOp	6 math math: geom_goldenRatio_isSol_fibRec, fibRec_charPoly_eq, geom_gold_isSol_fibRec, geom_goldConj_isSol_fibRec, fib_isSol_fibRec, geom_goldenConj_isSol_fibRec
goldenConj 📖	CompOp	35 math math: goldenConj_irrational, goldenConj_mul_fib_succ_add_fib, gold_add_goldConj, goldConj_sq, goldenRatio_mul_goldenConj, inv_goldenConj, one_sub_gold, gold_mul_goldConj, inv_goldenRatio, neg_one_lt_goldenConj, one_sub_goldConj, coe_fib_eq, goldConj_irrational, gold_sub_goldConj, goldenConj_mul_goldenRatio, Finset.doubling_lt_golden_ratio, coe_intFib_eq, tendsto_fib_div_fib_succ_atTop, geom_goldConj_isSol_fibRec, goldenConj_neg, goldenRatio_add_goldenConj, one_sub_goldenConj, goldenConj_sq, coe_fib_eq', goldConj_neg, inv_gold, fib_golden_conj_exp, neg_one_lt_goldConj, goldenRatio_sub_goldenConj, goldConj_mul_gold, fib_succ_sub_goldenConj_mul_fib, fib_succ_sub_goldenRatio_mul_fib, one_sub_goldenRatio, geom_goldenConj_isSol_fibRec, inv_goldConj
goldenRatio 📖	CompOp	39 math math: gold_sq, gold_add_goldConj, geom_goldenRatio_isSol_fibRec, goldenRatio_mul_goldenConj, goldenRatio_lt_two, inv_goldenConj, one_sub_gold, gold_mul_goldConj, inv_goldenRatio, one_lt_goldenRatio, goldenRatio_irrational, one_sub_goldConj, fib_golden_exp', geom_gold_isSol_fibRec, goldenRatio_pow_sub_goldenRatio_pow, coe_fib_eq, gold_sub_goldConj, goldenConj_mul_goldenRatio, goldenRatio_mul_fib_succ_add_fib, one_lt_gold, coe_intFib_eq, goldenRatio_add_goldenConj, goldenRatio_pos, one_sub_goldenConj, coe_fib_eq', inv_gold, fib_golden_conj_exp, gold_lt_two, tendsto_fib_succ_div_fib_atTop, goldenRatio_sub_goldenConj, goldConj_mul_gold, gold_pos, fib_succ_sub_goldenConj_mul_fib, fib_succ_sub_goldenRatio_mul_fib, gold_irrational, gold_pow_sub_gold_pow, one_sub_goldenRatio, goldenRatio_sq, inv_goldConj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_fib_eq 📖	mathematical	—	Real instNatCast Nat.fib DivInvMonoid.toDiv instDivInvMonoid instSub Monoid.toNatPow instMonoid goldenRatio goldenConj sqrt instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat coe_fib_eq'
coe_fib_eq' 📖	mathematical	—	Real instNatCast Nat.fib DivInvMonoid.toDiv instDivInvMonoid instSub Monoid.toNatPow instMonoid goldenRatio goldenConj sqrt instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat LinearRecurrence.sol_eq_of_eq_init fib_isSol_fibRec Submodule.sub_mem Submodule.smul_mem geom_goldenRatio_isSol_fibRec geom_goldenConj_isSol_fibRec Pi.sub_apply Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr CharP.cast_eq_zero CharP.ofCharZero pow_zero sub_self zero_div Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_fib Nat.fib_one Mathlib.Tactic.RingNF.nat_rawCast_1 add_zero Mathlib.Tactic.Ring.pow_one_cast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNNRat_add pow_one mul_one mul_inv_cancel₀ Mathlib.Meta.NormNum.isNat_le_true instIsOrderedRing Nat.cast_zero Mathlib.Meta.NormNum.isNat_eq_false
coe_intFib_eq 📖	mathematical	—	Real instIntCast Int.fib DivInvMonoid.toDiv instDivInvMonoid instSub DivInvMonoid.toZPow goldenRatio goldenConj sqrt instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat coe_fib_eq Int.fib_neg Int.cast_ite Int.cast_neg Int.cast_natCast zpow_neg zpow_natCast inv_goldenRatio neg_one_mul mul_pow neg_one_pow_eq_ite inv_goldenConj
fibRec_charPoly_eq 📖	mathematical	—	LinearRecurrence.charPoly fibRec CommRing.toCommSemiring Polynomial CommSemiring.toSemiring Polynomial.instSub CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Polynomial.instAdd Polynomial.instOne	—	fibRec.eq_1 LinearRecurrence.charPoly.eq_1 one_smul Finset.sum_congr Finset.sum_fin_eq_sum_range Finset.sum_range_succ' Matrix.cons_val_succ' Matrix.cons_val_fin_one Finset.sum_singleton zero_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat pow_one IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial pow_zero
fib_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution fibRec AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Nat.fib	—	fibRec.eq_1 Finset.sum_congr Nat.fib_add_two add_comm Nat.cast_add Finset.sum_fin_eq_sum_range Finset.sum_range_succ' Matrix.cons_val_succ' Matrix.cons_val_fin_one one_mul Finset.sum_singleton zero_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial add_zero
fib_succ_sub_goldenConj_mul_fib 📖	mathematical	—	Real instSub instNatCast Nat.fib instMul goldenConj Monoid.toNatPow instMonoid goldenRatio	—	—
fib_succ_sub_goldenRatio_mul_fib 📖	mathematical	—	Real instSub instNatCast Nat.fib instMul goldenRatio Monoid.toNatPow instMonoid goldenConj	—	Nat.instAtLeastTwoHAddOfNat coe_fib_eq mul_div div_sub_div_same mul_sub pow_succ' Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.inv_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero mul_one Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Meta.NormNum.isNat_le_true instIsOrderedRing Nat.cast_zero Mathlib.Meta.NormNum.isNat_eq_false mul_inv_cancel₀ one_mul
geom_goldConj_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution Real instCommSemiring fibRec Monoid.toNatPow instMonoid goldenConj	—	geom_goldenConj_isSol_fibRec
geom_goldenConj_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution Real instCommSemiring fibRec Monoid.toNatPow instMonoid goldenConj	—	LinearRecurrence.geom_sol_iff_root_charPoly fibRec_charPoly_eq Polynomial.eval_sub Polynomial.eval_pow Polynomial.eval_X goldenConj_sq Polynomial.eval_add Polynomial.eval_one sub_self
geom_goldenRatio_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution Real instCommSemiring fibRec Monoid.toNatPow instMonoid goldenRatio	—	LinearRecurrence.geom_sol_iff_root_charPoly fibRec_charPoly_eq Polynomial.eval_sub Polynomial.eval_pow Polynomial.eval_X goldenRatio_sq Polynomial.eval_add Polynomial.eval_one sub_self
gold_pow_sub_gold_pow 📖	mathematical	—	Real instSub Monoid.toNatPow instMonoid goldenRatio	—	goldenRatio_pow_sub_goldenRatio_pow
goldenConj_irrational 📖	mathematical	—	Irrational goldenConj	—	Nat.Prime.irrational_sqrt Mathlib.Meta.NormNum.isNat_prime_2 Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_minFac_4 Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.minFacHelper_0 Irrational.ratCast_sub Nat.instAtLeastTwoHAddOfNat Rat.cast_ofScientific Rat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_nnrat Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Irrational.ratCast_mul Mathlib.Meta.NormNum.isNNRat_eq_false
goldenConj_mul_fib_succ_add_fib 📖	mathematical	—	Real instAdd instMul goldenConj instNatCast Nat.fib Monoid.toNatPow instMonoid	—	—
goldenConj_mul_goldenRatio 📖	mathematical	—	Real instMul goldenConj goldenRatio instNeg instOne	—	mul_comm goldenRatio_mul_goldenConj
goldenConj_ne_zero 📖	—	—	—	—	ne_of_lt goldenConj_neg
goldenConj_neg 📖	mathematical	—	Real instLT goldenConj instZero	—	lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.le_of_le_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing neg_eq_zero sub_eq_zero_of_eq one_sub_goldenConj Mathlib.Tactic.Linarith.sub_neg_of_lt one_lt_goldenRatio
goldenConj_sq 📖	mathematical	—	Real Monoid.toNatPow instMonoid goldenConj instAdd instOne	—	—
goldenRatio_add_goldenConj 📖	mathematical	—	Real instAdd goldenRatio goldenConj instOne	—	goldenRatio.eq_1 goldenConj.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz
goldenRatio_irrational 📖	mathematical	—	Irrational goldenRatio	—	Nat.Prime.irrational_sqrt Mathlib.Meta.NormNum.isNat_prime_2 Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_minFac_4 Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.minFacHelper_0 Irrational.ratCast_add Nat.instAtLeastTwoHAddOfNat Rat.cast_ofScientific Rat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_nnrat Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Irrational.ratCast_mul Mathlib.Meta.NormNum.isNNRat_eq_false
goldenRatio_lt_two 📖	mathematical	—	Real instLT goldenRatio instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sqrt_lt' Mathlib.Meta.NormNum.isNat_lt_true instIsOrderedRing IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNat_add Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos
goldenRatio_mul_fib_succ_add_fib 📖	mathematical	—	Real instAdd instMul goldenRatio instNatCast Nat.fib Monoid.toNatPow instMonoid	—	zero_add Nat.cast_one mul_one CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero instIsStrictOrderedRing add_zero pow_one Nat.fib_add_one tsub_zero Nat.instOrderedSub Nat.cast_add goldenRatio_sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.pow_zero add_comm Mathlib.Tactic.Ring.pow_atom
goldenRatio_mul_goldenConj 📖	mathematical	—	Real instMul goldenRatio goldenConj instNeg instOne	—	—
goldenRatio_ne_zero 📖	—	—	—	—	ne_of_gt goldenRatio_pos
goldenRatio_pos 📖	mathematical	—	Real instLT instZero goldenRatio	—	mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.NormNum.isNat_lt_true instIsOrderedRing IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE zero_lt_two instZeroLEOneClass NeZero.charZero_one
goldenRatio_pow_sub_goldenRatio_pow 📖	mathematical	—	Real instSub Monoid.toNatPow instMonoid goldenRatio	—	—
goldenRatio_sq 📖	mathematical	—	Real Monoid.toNatPow instMonoid goldenRatio instAdd instOne	—	—
goldenRatio_sub_goldenConj 📖	mathematical	—	Real instSub goldenRatio goldenConj sqrt instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Mathlib.Tactic.Ring.of_eq Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add
inv_goldenConj 📖	mathematical	—	Real instInv goldenConj instNeg goldenRatio	—	inv_eq_iff_eq_inv neg_inv neg_eq_iff_eq_neg inv_goldenRatio
inv_goldenRatio 📖	mathematical	—	Real instInv goldenRatio instNeg goldenConj	—	—
neg_one_lt_goldenConj 📖	mathematical	—	Real instLT instNeg instOne goldenConj	—	neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add inv_goldenRatio inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instZeroLEOneClass one_lt_goldenRatio
one_lt_goldenRatio 📖	mathematical	—	Real instLT instOne goldenRatio	—	lt_of_mul_lt_mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing mul_one goldenRatio_sq IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_lt_of_covariant_le instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero le_of_lt goldenRatio_pos
one_sub_goldenConj 📖	mathematical	—	Real instSub instOne goldenRatio goldenConj	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing sub_eq_zero_of_eq goldenRatio_add_goldenConj Mathlib.Tactic.Ring.neg_congr neg_eq_zero
one_sub_goldenRatio 📖	mathematical	—	Real instSub instOne goldenConj goldenRatio	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing sub_eq_zero_of_eq goldenRatio_add_goldenConj Mathlib.Tactic.Ring.neg_congr neg_eq_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fib_golden_conj_exp 📖	mathematical	—	Real Real.instSub Real.instNatCast Nat.fib Real.instMul Real.goldenRatio Monoid.toNatPow Real.instMonoid Real.goldenConj	—	Real.fib_succ_sub_goldenRatio_mul_fib
fib_golden_exp' 📖	mathematical	—	Real Real.instAdd Real.instMul Real.goldenRatio Real.instNatCast Nat.fib Monoid.toNatPow Real.instMonoid	—	Real.goldenRatio_mul_fib_succ_add_fib
geom_gold_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution Real Real.instCommSemiring Real.fibRec Monoid.toNatPow Real.instMonoid Real.goldenRatio	—	Real.geom_goldenRatio_isSol_fibRec
goldConj_irrational 📖	mathematical	—	Irrational Real.goldenConj	—	Real.goldenConj_irrational
goldConj_mul_gold 📖	mathematical	—	Real Real.instMul Real.goldenConj Real.goldenRatio Real.instNeg Real.instOne	—	Real.goldenConj_mul_goldenRatio
goldConj_ne_zero 📖	—	—	—	—	Real.goldenConj_ne_zero
goldConj_neg 📖	mathematical	—	Real Real.instLT Real.goldenConj Real.instZero	—	Real.goldenConj_neg
goldConj_sq 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid Real.goldenConj Real.instAdd Real.instOne	—	Real.goldenConj_sq
gold_add_goldConj 📖	mathematical	—	Real Real.instAdd Real.goldenRatio Real.goldenConj Real.instOne	—	Real.goldenRatio_add_goldenConj
gold_irrational 📖	mathematical	—	Irrational Real.goldenRatio	—	Real.goldenRatio_irrational
gold_lt_two 📖	mathematical	—	Real Real.instLT Real.goldenRatio instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.goldenRatio_lt_two
gold_mul_goldConj 📖	mathematical	—	Real Real.instMul Real.goldenRatio Real.goldenConj Real.instNeg Real.instOne	—	Real.goldenRatio_mul_goldenConj
gold_ne_zero 📖	—	—	—	—	Real.goldenRatio_ne_zero
gold_pos 📖	mathematical	—	Real Real.instLT Real.instZero Real.goldenRatio	—	Real.goldenRatio_pos
gold_sq 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid Real.goldenRatio Real.instAdd Real.instOne	—	Real.goldenRatio_sq
gold_sub_goldConj 📖	mathematical	—	Real Real.instSub Real.goldenRatio Real.goldenConj Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.goldenRatio_sub_goldenConj
inv_gold 📖	mathematical	—	Real Real.instInv Real.goldenRatio Real.instNeg Real.goldenConj	—	Real.inv_goldenRatio
inv_goldConj 📖	mathematical	—	Real Real.instInv Real.goldenConj Real.instNeg Real.goldenRatio	—	Real.inv_goldenConj
neg_one_lt_goldConj 📖	mathematical	—	Real Real.instLT Real.instNeg Real.instOne Real.goldenConj	—	Real.neg_one_lt_goldenConj
one_lt_gold 📖	mathematical	—	Real Real.instLT Real.instOne Real.goldenRatio	—	Real.one_lt_goldenRatio
one_sub_gold 📖	mathematical	—	Real Real.instSub Real.instOne Real.goldenConj Real.goldenRatio	—	Real.one_sub_goldenRatio
one_sub_goldConj 📖	mathematical	—	Real Real.instSub Real.instOne Real.goldenRatio Real.goldenConj	—	Real.one_sub_goldenConj

goldenRatio

Definitions

Name	Category	Theorems
termφ 📖	CompOp	—
termψ 📖	CompOp	—

---

← Back to Index