Documentation Verification Report

GoldenRatio

πŸ“ Source: Mathlib/NumberTheory/Real/GoldenRatio.lean

Statistics

MetricCount
DefinitionsfibRec, goldenConj, goldenRatio, termΟ†, termψ
5
Theoremscoe_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
Total60

Real

Definitions

NameCategoryTheorems
fibRec πŸ“–CompOp
6 mathmath: 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 mathmath: 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 mathmath: 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

NameKindAssumesProvesValidatesDepends 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

NameKindAssumesProvesValidatesDepends 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

NameCategoryTheorems
termΟ† πŸ“–CompOpβ€”
termψ πŸ“–CompOpβ€”

---

← Back to Index