U (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

U (Lemmas)

ubnP [prf, in mathcomp.boot.ssrnat]
ubnPeq [prf, in mathcomp.boot.ssrnat]
ubnPgeq [prf, in mathcomp.boot.ssrnat]
ubnPleq [prf, in mathcomp.boot.ssrnat]
ucn0 [prf, in mathcomp.solvable.nilpotent]
ucn1 [prf, in mathcomp.solvable.nilpotent]
ucn_bigcprod [prf, in mathcomp.solvable.nilpotent]
ucn_bigdprod [prf, in mathcomp.solvable.nilpotent]
ucn_central [prf, in mathcomp.solvable.nilpotent]
ucn_char [prf, in mathcomp.solvable.nilpotent]
ucn_comm [prf, in mathcomp.solvable.nilpotent]
ucn_cprod [prf, in mathcomp.solvable.nilpotent]
ucn_dprod [prf, in mathcomp.solvable.nilpotent]
ucn_group_set [prf, in mathcomp.solvable.nilpotent]
ucn_id [prf, in mathcomp.solvable.nilpotent]
ucn_lcnP [prf, in mathcomp.solvable.nilpotent]
ucn_nil_classP [prf, in mathcomp.solvable.nilpotent]
ucn_nilpotent [prf, in mathcomp.solvable.nilpotent]
ucn_norm [prf, in mathcomp.solvable.nilpotent]
ucn_normal [prf, in mathcomp.solvable.nilpotent]
ucn_normalS [prf, in mathcomp.solvable.nilpotent]
ucn_pmap [prf, in mathcomp.solvable.nilpotent]
ucn_sub [prf, in mathcomp.solvable.nilpotent]
ucn_sub_geq [prf, in mathcomp.solvable.nilpotent]
ucn_subS [prf, in mathcomp.solvable.nilpotent]
ucnE [prf, in mathcomp.solvable.nilpotent]
ucnP [prf, in mathcomp.solvable.nilpotent]
ucnSn [prf, in mathcomp.solvable.nilpotent]
ucnSnR [prf, in mathcomp.solvable.nilpotent]
ucycle_cycle [prf, in mathcomp.boot.path]
ucycle_uniq [prf, in mathcomp.boot.path]
ulsubmx_diag [prf, in mathcomp.algebra.matrix]
ulsubmx_trig [prf, in mathcomp.algebra.matrix]
ulsubmxEsub [prf, in mathcomp.algebra.matrix]
unbumpDl [prf, in mathcomp.boot.fintype]
unbumpK [prf, in mathcomp.boot.fintype]
unbumpKcond [prf, in mathcomp.boot.fintype]
unbumpS [prf, in mathcomp.boot.fintype]
undup_cat [prf, in mathcomp.boot.seq]
undup_cycle_cons [prf, in mathcomp.boot.fingraph]
undup_flatten_nseq [prf, in mathcomp.boot.seq]
undup_id [prf, in mathcomp.boot.seq]
undup_map_inj [prf, in mathcomp.boot.seq]
undup_nil [prf, in mathcomp.boot.seq]
undup_path [prf, in mathcomp.boot.path]
undup_rcons [prf, in mathcomp.boot.seq]
undup_sorted [prf, in mathcomp.boot.path]
undup_subseq [prf, in mathcomp.boot.seq]
undup_uniq [prf, in mathcomp.boot.seq]
uniq4_uniq6 [prf, in mathcomp.solvable.burnside_app]
uniq_cat_inLR [prf, in mathcomp.boot.seq]
uniq_cat_inRL [prf, in mathcomp.boot.seq]
uniq_catC [prf, in mathcomp.boot.seq]
uniq_catCA [prf, in mathcomp.boot.seq]
uniq_eqseq_pivotl [prf, in mathcomp.boot.seq]
uniq_eqseq_pivotr [prf, in mathcomp.boot.seq]
uniq_leq_size [prf, in mathcomp.boot.seq]
uniq_map_inj_in [prf, in mathcomp.boot.seq]
uniq_min_size [prf, in mathcomp.boot.seq]
uniq_normal_Hall [prf, in mathcomp.solvable.pgroup]
uniq_pairwise [prf, in mathcomp.boot.seq]
uniq_perm [prf, in mathcomp.boot.seq]
uniq_roots_prod_XsubC [prf, in mathcomp.algebra.poly]
uniq_rootsE [prf, in mathcomp.algebra.poly]
uniq_size_uniq [prf, in mathcomp.boot.seq]
uniq_sub_le_big [prf, in mathcomp.boot.bigop]
uniq_sub_le_big_cond [prf, in mathcomp.boot.bigop]
uniq_subseq_pivot [prf, in mathcomp.boot.seq]
uniq_traject_porbit [prf, in mathcomp.finite_group.perm]
uniqP [prf, in mathcomp.boot.seq]
uniqPn [prf, in mathcomp.boot.seq]
unit_enumP [prf, in mathcomp.boot.fintype]
unit_eqP [prf, in mathcomp.boot.eqtype]
unit_Zp_expg [prf, in mathcomp.algebra.zmodp]
unit_Zp_mulgC [prf, in mathcomp.algebra.zmodp]
unitarymx_key [prf, in mathcomp.algebra.spectral]
unitarymx_unit [prf, in mathcomp.algebra.spectral]
unitarymxP [prf, in mathcomp.algebra.spectral]
unitFpE [prf, in mathcomp.algebra.zmodp]
unitmx1 [prf, in mathcomp.algebra.matrix]
unitmx_inv [prf, in mathcomp.algebra.matrix]
unitmx_mul [prf, in mathcomp.algebra.matrix]
unitmx_perm [prf, in mathcomp.algebra.matrix]
unitmx_tr [prf, in mathcomp.algebra.matrix]
unitmxE [prf, in mathcomp.algebra.matrix]
unitmxZ [prf, in mathcomp.algebra.matrix]
unitr_algid1 [prf, in mathcomp.field.falgebra]
unitr_n0expz [prf, in mathcomp.algebra.ssrint]
unitr_trmx [prf, in mathcomp.algebra.matrix]
unitrXz [prf, in mathcomp.algebra.ssrint]
units_Zp_abelian [prf, in mathcomp.algebra.zmodp]
units_Zp_cyclic [prf, in mathcomp.solvable.cyclic]
unity_rootE [prf, in mathcomp.algebra.poly]
unity_rootP [prf, in mathcomp.algebra.poly]
unitZpE [prf, in mathcomp.algebra.zmodp]
unlift_none [prf, in mathcomp.boot.fintype]
unlift_some [prf, in mathcomp.boot.fintype]
unliftP [prf, in mathcomp.boot.fintype]
unset10 [prf, in mathcomp.boot.finset]
unset1K [prf, in mathcomp.boot.finset]
unset1N1 [prf, in mathcomp.boot.finset]
unsplitK [prf, in mathcomp.boot.fintype]
untag_cst [prf, in mathcomp.boot.eqtype]
untag_dflt [prf, in mathcomp.boot.eqtype]
untag_with_bij [prf, in mathcomp.boot.eqtype]
untag_withK [prf, in mathcomp.boot.eqtype]
untagE [prf, in mathcomp.boot.eqtype]
unzip1_map_nth_zip [prf, in mathcomp.boot.seq]
unzip1_zip [prf, in mathcomp.boot.seq]
unzip2_map_nth_zip [prf, in mathcomp.boot.seq]
unzip2_zip [prf, in mathcomp.boot.seq]
up_expnK [prf, in mathcomp.boot.prime]
up_log0 [prf, in mathcomp.boot.prime]
up_log1 [prf, in mathcomp.boot.prime]
up_log2_double [prf, in mathcomp.boot.prime]
up_log2S [prf, in mathcomp.boot.prime]
up_log_bounds [prf, in mathcomp.boot.prime]
up_log_eq [prf, in mathcomp.boot.prime]
up_log_eq0 [prf, in mathcomp.boot.prime]
up_log_gt0 [prf, in mathcomp.boot.prime]
up_log_gtn [prf, in mathcomp.boot.prime]
up_log_min [prf, in mathcomp.boot.prime]
up_log_trunc_log [prf, in mathcomp.boot.prime]
up_logMp [prf, in mathcomp.boot.prime]
up_lognn [prf, in mathcomp.boot.prime]
up_logP [prf, in mathcomp.boot.prime]
uphalf_double [prf, in mathcomp.boot.ssrnat]
uphalf_gt0 [prf, in mathcomp.boot.ssrnat]
uphalf_half [prf, in mathcomp.boot.ssrnat]
uphalf_leq [prf, in mathcomp.boot.ssrnat]
uphalfE [prf, in mathcomp.boot.ssrnat]
uphalfK [prf, in mathcomp.boot.ssrnat]
ursubmx_trig [prf, in mathcomp.algebra.matrix]
ursubmxEsub [prf, in mathcomp.algebra.matrix]
usubmx_key [prf, in mathcomp.algebra.matrix]
usubmxEsub [prf, in mathcomp.algebra.matrix]
usumx_mul [prf, in mathcomp.group_representation.character]