theorem
proved
wrapper
rs_kappa_pos
show as:
view Lean formalization →
formal statement (Lean)
219theorem rs_kappa_pos : 0 < rs_kappa := by
proof body
One-line wrapper that applies unfold.
220 unfold rs_kappa; exact mul_pos (by norm_num) (pow_pos phi_pos 5)
221