No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
46lemma phi_eq_one_add_inv_phi : phi = 1 + (1 : ℝ) / phi := by
proof body
Tactic-mode proof.
47 have hphi_ne_zero : phi ≠ 0 := phi_ne_zero
48 calc
49 phi = phi ^ 2 / phi := by
50 field_simp [hphi_ne_zero]
51 _ = (phi + 1) / phi := by simp [phi_sq_eq]
52 _ = 1 + (1 : ℝ) / phi := by
53 field_simp [hphi_ne_zero]
54
55/-- Equivalent rewrite of `1 + 1/φ = φ`. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
phi_ne_zero
in IndisputableMonolith.Constants
decl_use
-
phi_sq_eq
in IndisputableMonolith.Constants
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
phi_ne_zero
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
phi_sq_eq
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
phi_ne_zero
in IndisputableMonolith.PhiSupport.Lemmas
decl_use
-
phi_eq_one_add_inv_phi
in IndisputableMonolith.RSBridge.GapFunctionForcing
decl_use