linear map on basis

Stream: maths

[orlando]

Hello,

do you have an idea for the sorry ? My fonction $\theta$ is define with if then else and i don't know how to deal with ! Perhaps something by case ? Perhaps my starting point is not good !

 import linear_algebra.basis linear_algebra.finite_dimensional
open is_basis linear_map
example {K : Type} {V : Type} [field K] [add_comm_group V] [vector_space K V]
[finite_dimensional K V](B : fin 3 → V)(hv : is_basis K B) : true :=
begin
   let θ : fin 3 → V := λ a, if a ≤ 1 then (B a) else 0,
   let φ := constr hv θ,
   have R : linear_map.comp φ φ = φ ,
   apply is_basis.ext hv,
   intro i,
   rw comp_apply,
   rw constr_basis,
        sorry,
   trivial,
 end

The tactic state before sorry is :

2 goals
K V : Type,
_inst_1 : field K,
_inst_2 : add_comm_group V,
_inst_3 : vector_space K V,
_inst_4 : finite_dimensional K V,
B : fin 3 → V,
hv : is_basis K B,
θ : fin 3 → V := λ (a : fin 3), ite (a ≤ 1) (B a) 0,
φ : V →ₗ[K] V := constr hv θ,
i : fin 3
⊢ ⇑φ (θ i) = θ i

[Kenny Lau]

dsimp only [θ]; split_ifs

[orlando]

Good @Kenny Lau :+1: