Theorem: IsLinearMap.isLinearMap_const_zero (SciLean/Core/FunctionPropositions/IsLinearMap.lean)

State before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.6113
ι : Type ?u.6116
E : ι → Type ?u.6121
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module R X
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module R Y
inst✝³ : AddCommGroup Z
inst✝² : Module R Z
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ IsLinearMap R fun x => 0
Tactic:
sorry_proof
State after:
no goals