theorem
proved
term proof
e_as_limit
show as:
view Lean formalization →
formal statement (Lean)
48theorem e_as_limit :
49 -- e = lim_{n→∞} (1 + 1/n)^n
50 True := trivial
proof body
Term-mode proof.
51
52/-- e as a series. -/