proposition: Lemma fixedSpaceP f a : reflect (f a = a) (a \in fixedSpace f).
proof: Proof. by rewrite memv_ker add_lfunE opp_lfunE id_lfunE subr_eq0; apply: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)