Stream: maths

Topic: linear map on basis

orlando (May 01 2020 at 06:47):

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_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 (May 01 2020 at 06:49):

dsimp only [θ]; split_ifs

orlando (May 01 2020 at 06:54):

Good @Kenny Lau :+1:

Last updated: May 10 2021 at 06:13 UTC