α : Type u_2
β : Type ?u.1368
m : Type ?u.1371
n : Type u_1
R : Type ?u.1377
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
⊢ v = w
α : Type u_2
β : Type ?u.1368
m : Type ?u.1371
n : Type u_1
R : Type ?u.1377
inst✝ : AddGroup n
⊢ Injective circulant
intro v w h
case h
α : Type u_2
β : Type ?u.1368
m : Type ?u.1371
n : Type u_1
R : Type ?u.1377
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k
α : Type u_2
β : Type ?u.1368
m : Type ?u.1371
n : Type u_1
R : Type ?u.1377
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
⊢ v = w
ext k
no goals
case h
α : Type u_2
β : Type ?u.1368
m : Type ?u.1371
n : Type u_1
R : Type ?u.1377
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k
rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]