case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ (circulant v ⬝ circulant w) i j = circulant (mulVec (circulant v) w) i j
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
⊢ circulant v ⬝ circulant w = circulant (mulVec (circulant v) w)
ext (i j)
case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, v (i - j - x) * w x
case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ (circulant v ⬝ circulant w) i j = circulant (mulVec (circulant v) w) i j
simp only [mul_apply, mulVec, circulant_apply, dotProduct]
case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∀ (x : n), v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, v (i - j - x) * w x
refine' Fintype.sum_equiv (Equiv.subRight j) _ _ _
case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∀ (x : n), v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
intro x
no goals
case a.h
α : Type u_1
β : Type ?u.17976
m : Type ?u.17979
n : Type u_2
R : Type ?u.17985
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]