lemma proved term proof

`G_ne_zero`

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)

  41lemma G_ne_zero : G ≠ 0 := ne_of_gt G_pos

proof body

Term-mode proof.

  42
  43end
  44
  45end Constants
  46end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G_pos in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G_pos in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
G_pos in IndisputableMonolith.Foundation.ConstantDerivations decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use