Theorem: Point.add_z (LeanCourse/Lectures/Lecture8Before.lean)

State before:
n : ℕ
a b : Point
⊢ (a + b).z = a.z + b.z
Tactic:
rfl
State after:
no goals