proposition: Fact algid_decidable U : decidable (exists e, is_algid e U).
proof: Proof. have [-> | nzU] := eqVneq U 0%VS. by right=> [[e []]]; rewrite memv0 => ->. pose X := vbasis U; pose feq f1 f2 := [tuple of map f1 X ++ map f2 X]. have feqL f i: tnth (feq _ f _) (lshift _ i) = f X`_i. set v := f _; rewrite (tnth_nth v) /= nth_cat size_map size_tuple. by rewrite ltn_ord (nth_map 0) ?size_tuple. have feqR f i: tnth (feq _ _ f) (rshift _ i) = f X`_i. set v := f _; rewrite (tnth_nth v) /= nth_cat size_map size_tuple. by rewrite ltnNge leq_addr addKn /= (nth_map 0) ?size_tuple. apply: decP (vsolve_eq (feq _ amulr amull) (feq _ id id) U) _. apply: (iffP (vsolve_eqP _ _ _)) => [[e Ue id_e] | [e [Ue _ id_e]]]. suffices idUe: {in U, forall u, e * u = u /\ u * e = u}. exists e; split=> //; apply: contraNneq nzU => e0; rewrite -subv0. by apply/subvP=> u /idUe[<- _]; rewrite e0 mul0r mem0v. move=> u /coord_vbasis->; rewrite mulr_sumr mulr_suml. split; apply/eq_bigr=> i _; rewrite -(scalerAr, scalerAl); congr (_ *: _). by have:= id_e (lshift _ i); rewrite !feqL lfunE. by have:= id_e (rshift _ i); rewrite !feqR lfunE. have{id_e} /all_and2[ideX idXe]:= id_e _ (vbasis_mem (mem_tnth _ X)). exists e => // k; rewrite -[k]splitK. by case: (split k) => i; rewrite !(feqL, feqR) lfunE /= -tnth_nth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)