no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : i = j
⊢ slice (unitVec d j ⊗ x) i hid t = ite (i = j) x 0 t
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = OfNat.ofNat 0 t
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ slice (unitVec d j ⊗ x) i hid t = ite (i = j) x 0 t
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]
no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = OfNat.ofNat 0 t
rfl