Theorem: SciLean.oneHot.arg_xi.IsLinearMap_rule (SciLean/Data/StructType/Algebra.lean)

State before:
K : Type u_1
inst✝¹⁴ : RCLike K
ι : Type ?u.178721
κ : Type ?u.178724
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.178771
I : Type u_5
EI : I → Type ?u.178779
inst✝⁷ : StructType E I EI
F : Type ?u.178790
J : Type ?u.178793
FJ : J → Type ?u.178798
inst✝⁶ : StructType F J FJ
X : Type u_4
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type u_2
inst✝ : Vec K W
i : I
xi : W → XI i
hxi : IsLinearMap K xi
⊢ IsLinearMap K fun w => oneHot i (xi w)
Tactic:
fun_prop
State after:
no goals