def
definition
def or abbrev
gamma_pot
show as:
view Lean formalization →
formal statement (Lean)
10noncomputable def gamma_pot (ψ : RefreshField) (p : ILGParams) : ℝ := 1