Zulip Chat Archive

Stream: maths

Topic: linear map on basis


view this post on Zulip 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_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

view this post on Zulip Kenny Lau (May 01 2020 at 06:49):

dsimp only [θ]; split_ifs

view this post on Zulip orlando (May 01 2020 at 06:54):

Good @Kenny Lau :+1:


Last updated: May 10 2021 at 06:13 UTC