theorem
proved
term proof
canonical_g2FromLoops
show as:
view Lean formalization →
formal statement (Lean)
63theorem canonical_g2FromLoops (φ : ℝ) :
64 g2FromLoops (canonicalRSBridge L) φ = 1 / (φ ^ 5) := by
proof body
Term-mode proof.
65 simp [g2FromLoops, canonicalRSBridge]
66
67end
68
69end RecogSpec
70end IndisputableMonolith