pith. machine review for the scientific record. sign in
lemma proved term proof

curvature_at_identity

show as:
view Lean formalization →

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)

 118lemma curvature_at_identity : possibility_curvature (identity_config 0) = 2 := by

proof body

Term-mode proof.

 119  simp only [possibility_curvature, identity_config, inv_one, one_pow]
 120  ring
 121
 122/-- Curvature is positive everywhere. -/

depends on (6)

Lean names referenced from this declaration's body.