theorem
other
other
upsilon_star_eq_phi
show as:
view Lean formalization →
formal statement (Lean)
76theorem upsilon_star_eq_phi : upsilon_star = phi := rfl
proof body
77