Theorem: Weight.w1_zero (Weights/Degree1.lean)

State before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ w1 n 0 = 0
Tactic:
simp only [w1, eq_self_iff_true, if_true]
State after:
no goals