lemma
other
other
z_t_zero
show as:
view Lean formalization →
formal statement (Lean)
74@[simp] lemma z_t_zero : z t_entry = 0 := by simp [z]
proof body
75