no goals
α✝ : Type ?u.59587
β : Type ?u.59590
m : Type ?u.59593
n : Type ?u.59596
R : Type ?u.59599
α : Type u_1
inst✝¹ : Zero α
inst✝ : One α
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1
simp [Injective]
α✝ : Type ?u.59587
β : Type ?u.59590
m : Type ?u.59593
n✝ : Type ?u.59596
R : Type ?u.59599
α : Type u_1
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = circulant (Pi.single 0 1)
α✝ : Type ?u.59587
β : Type ?u.59590
m : Type ?u.59593
n✝ : Type ?u.59596
R : Type ?u.59599
α : Type u_1
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1
rw [← circulant_single_one]
case a.h
α✝ : Type ?u.59587
β : Type ?u.59590
m : Type ?u.59593
n✝ : Type ?u.59596
R : Type ?u.59599
α : Type u_1
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
j x✝ : Fin (n + 1)
⊢ circulant (fun i => if ↑i = 0 then 1 else 0) j x✝ = circulant (Pi.single 0 1) j x✝
α✝ : Type ?u.59587
β : Type ?u.59590
m : Type ?u.59593
n✝ : Type ?u.59596
R : Type ?u.59599
α : Type u_1
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = circulant (Pi.single 0 1)
congr with j
no goals
case a.h
α✝ : Type ?u.59587
β : Type ?u.59590
m : Type ?u.59593
n✝ : Type ?u.59596
R : Type ?u.59599
α : Type u_1
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
j x✝ : Fin (n + 1)
⊢ circulant (fun i => if ↑i = 0 then 1 else 0) j x✝ = circulant (Pi.single 0 1) j x✝
simp [Pi.single_apply, Fin.ext_iff]