case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v ⬝ circulant w) i j = (circulant w ⬝ circulant v) i j
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
⊢ circulant v ⬝ circulant w = circulant w ⬝ circulant v
ext (i j)
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, w (i - x) * v (x - j)
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v ⬝ circulant w) i j = (circulant w ⬝ circulant v) i j
simp only [mul_apply, circulant_apply, mul_comm]
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∀ (x : n),
    v (i - x) * w (x - j) =
      w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, w (i - x) * v (x - j)
refine' Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ _
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) =
    w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∀ (x : n),
    v (i - x) * w (x - j) =
      w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
intro x
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) =
    w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
simp [mul_comm]
case a.h.e_a.e_a
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)
case a.h
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
congr 2
no goals
case a.h.e_a.e_a
α : Type u_1
β : Type ?u.24908
m : Type ?u.24911
n : Type u_2
R : Type ?u.24917
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)
abel