case a.h
α : Type u_2
β : Type ?u.43737
m : Type ?u.43740
n✝ : Type ?u.43743
R : Type ?u.43746
n : Type u_1
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
i j : n
⊢ circulant (Pi.single 0 a) i j = ↑(scalar n) a i j
α : Type u_2
β : Type ?u.43737
m : Type ?u.43740
n✝ : Type ?u.43743
R : Type ?u.43746
n : Type u_1
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
⊢ circulant (Pi.single 0 a) = ↑(scalar n) a
ext (i j)
no goals
case a.h
α : Type u_2
β : Type ?u.43737
m : Type ?u.43740
n✝ : Type ?u.43743
R : Type ?u.43746
n : Type u_1
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
i j : n
⊢ circulant (Pi.single 0 a) i j = ↑(scalar n) a i j
simp [Pi.single_apply, one_apply, sub_eq_zero]