theorem
other
other
row_fermi_pred_eq
show as:
view Lean formalization →
formal statement (Lean)
56theorem row_fermi_pred_eq :
57 row_fermi_pred = 1 / (Real.sqrt 2 * vev_canonical ^ 2) := rfl
proof body
58