case a.h
α✝ : Type ?u.41028
β : Type ?u.41031
m : Type ?u.41034
n✝ : Type ?u.41037
R : Type ?u.41040
α : Type u_1
n : Type u_2
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = OfNat.ofNat 1 i j
α✝ : Type ?u.41028
β : Type ?u.41031
m : Type ?u.41034
n✝ : Type ?u.41037
R : Type ?u.41040
α : Type u_1
n : Type u_2
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
⊢ circulant (Pi.single 0 1) = 1
ext (i j)
no goals
case a.h
α✝ : Type ?u.41028
β : Type ?u.41031
m : Type ?u.41034
n✝ : Type ?u.41037
R : Type ?u.41040
α : Type u_1
n : Type u_2
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = OfNat.ofNat 1 i j
simp [one_apply, Pi.single_apply, sub_eq_zero]