Theorem: Weight.f_eq_on_shift (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ f (w + k • 1) = f w
Tactic:
ext a
State after:
case h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : ↑(testvecs n d)
⊢ f (w + k • 1) a = f w a

State before:
case h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : ↑(testvecs n d)
⊢ f (w + k • 1) a = f w a
Tactic:
simp only [f_apply, E_shift, pair_add_left, pair_shift, add_tsub_add_eq_tsub_right]
State after:
no goals