C (Lemmas)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
C (Lemmas)
C_prim_root_exists [prf, in mathcomp.field.cyclotomic]can2_eq [prf, in mathcomp.boot.eqtype]
can2_gmulf1 [prf, in mathcomp.boot.monoid]
can2_gmulfM [prf, in mathcomp.boot.monoid]
can2_imset_pre [prf, in mathcomp.boot.finset]
can2_in_imset_pre [prf, in mathcomp.boot.finset]
can2_mem_pmap [prf, in mathcomp.boot.seq]
can_eq [prf, in mathcomp.boot.eqtype]
can_imset_pre [prf, in mathcomp.boot.finset]
can_in_eq [prf, in mathcomp.boot.eqtype]
cancel_index_extremal_groups [prf, in mathcomp.solvable.extremal]
canF_eq [prf, in mathcomp.boot.fintype]
canF_invF [prf, in mathcomp.boot.fintype]
canF_LR [prf, in mathcomp.boot.fintype]
canF_RL [prf, in mathcomp.boot.fintype]
canF_sym [prf, in mathcomp.boot.fintype]
cap0mx [prf, in mathcomp.algebra.mxalgebra]
cap0v [prf, in mathcomp.algebra.vector]
cap1mx [prf, in mathcomp.algebra.mxalgebra]
cap_cfcenter_irr [prf, in mathcomp.group_representation.character]
cap_cfker_lin_irr [prf, in mathcomp.group_representation.character]
cap_cfker_normal [prf, in mathcomp.group_representation.character]
cap_eqmx [prf, in mathcomp.algebra.mxalgebra]
cap_genmx_ortho [prf, in mathcomp.algebra.spectral]
capfv [prf, in mathcomp.algebra.vector]
capmx0 [prf, in mathcomp.algebra.mxalgebra]
capmx1 [prf, in mathcomp.algebra.mxalgebra]
capmx_compl [prf, in mathcomp.algebra.mxalgebra]
capmx_diff [prf, in mathcomp.algebra.mxalgebra]
capmx_idPl [prf, in mathcomp.algebra.mxalgebra]
capmx_idPr [prf, in mathcomp.algebra.mxalgebra]
capmx_module [prf, in mathcomp.group_representation.mxrepresentation]
capmx_subSocle [prf, in mathcomp.group_representation.mxrepresentation]
capmxA [prf, in mathcomp.algebra.mxalgebra]
capmxC [prf, in mathcomp.algebra.mxalgebra]
capmxE [prf, in mathcomp.algebra.mxalgebra]
capmxMr [prf, in mathcomp.algebra.mxalgebra]
capmxS [prf, in mathcomp.algebra.mxalgebra]
capmxSl [prf, in mathcomp.algebra.mxalgebra]
capmxSr [prf, in mathcomp.algebra.mxalgebra]
capmxT [prf, in mathcomp.algebra.mxalgebra]
capTmx [prf, in mathcomp.algebra.mxalgebra]
capv0 [prf, in mathcomp.algebra.vector]
capv_compl [prf, in mathcomp.algebra.vector]
capv_diff [prf, in mathcomp.algebra.vector]
capv_idPl [prf, in mathcomp.algebra.vector]
capv_idPr [prf, in mathcomp.algebra.vector]
capvA [prf, in mathcomp.algebra.vector]
capvC [prf, in mathcomp.algebra.vector]
capvf [prf, in mathcomp.algebra.vector]
capvS [prf, in mathcomp.algebra.vector]
capvSl [prf, in mathcomp.algebra.vector]
capvSr [prf, in mathcomp.algebra.vector]
capvv [prf, in mathcomp.algebra.vector]
card0 [prf, in mathcomp.boot.fintype]
card0_eq [prf, in mathcomp.boot.fintype]
card1 [prf, in mathcomp.boot.fintype]
card1_trivg [prf, in mathcomp.finite_group.fingroup]
card1P [prf, in mathcomp.boot.fintype]
card2 [prf, in mathcomp.boot.fintype]
card_2dihedral [prf, in mathcomp.solvable.extremal]
card_abelem_rV [prf, in mathcomp.group_representation.mxabelem]
card_afix_irr_classes [prf, in mathcomp.group_representation.character]
card_Alt [prf, in mathcomp.solvable.alt]
card_Aut_cycle [prf, in mathcomp.solvable.cyclic]
card_Aut_cyclic [prf, in mathcomp.solvable.cyclic]
card_bool [prf, in mathcomp.boot.fintype]
card_bseq [prf, in mathcomp.boot.bigop]
card_center_extraspecial [prf, in mathcomp.solvable.maximal]
card_cfclass_Iirr [prf, in mathcomp.group_representation.inertia]
card_classes_abelian [prf, in mathcomp.finite_group.action]
card_codom [prf, in mathcomp.boot.fintype]
card_conjugates [prf, in mathcomp.finite_group.action]
card_cosetpre [prf, in mathcomp.finite_group.quotient]
card_dep_ffun [prf, in mathcomp.boot.finfun]
card_dihedral [prf, in mathcomp.solvable.extremal]
card_DnQ [prf, in mathcomp.solvable.extraspecial]
card_draws [prf, in mathcomp.boot.binomial]
card_ext_dihedral [prf, in mathcomp.solvable.extremal]
card_extraspecial [prf, in mathcomp.solvable.maximal]
card_family [prf, in mathcomp.boot.finfun]
card_ffun [prf, in mathcomp.boot.finfun]
card_ffun_on [prf, in mathcomp.boot.finfun]
card_Fid [prf, in mathcomp.solvable.burnside_app]
card_Fid3 [prf, in mathcomp.solvable.burnside_app]
card_finField_unit [prf, in mathcomp.field.finfield]
card_finField_unit [prf, in mathcomp.algebra.finalg]
card_finNzRing_gt1 [prf, in mathcomp.algebra.finalg]
card_finPcharP [prf, in mathcomp.field.finfield]
card_Fp [prf, in mathcomp.algebra.zmodp]
card_fprod [prf, in mathcomp.boot.finset]
card_fprod_u [prf, in mathcomp.algebra.tensor]
card_geqP [prf, in mathcomp.boot.fintype]
card_GL [prf, in mathcomp.algebra.mxalgebra]
card_GL_1 [prf, in mathcomp.algebra.mxalgebra]
card_GL_2 [prf, in mathcomp.algebra.mxalgebra]
card_gt0 [prf, in mathcomp.boot.finset]
card_gt0P [prf, in mathcomp.boot.fintype]
card_gt1P [prf, in mathcomp.boot.fintype]
card_gt2P [prf, in mathcomp.boot.fintype]
card_Hall [prf, in mathcomp.solvable.pgroup]
card_homg [prf, in mathcomp.finite_group.quotient]
card_homocyclic [prf, in mathcomp.solvable.abelian]
card_Iirr_abelian [prf, in mathcomp.group_representation.character]
card_Iirr_cyclic [prf, in mathcomp.group_representation.character]
card_im_injm [prf, in mathcomp.finite_group.morphism]
card_image [prf, in mathcomp.boot.fintype]
card_imset [prf, in mathcomp.boot.finset]
card_in_image [prf, in mathcomp.boot.fintype]
card_in_imset [prf, in mathcomp.boot.finset]
card_inj_ffuns [prf, in mathcomp.boot.binomial]
card_inj_ffuns_on [prf, in mathcomp.boot.binomial]
card_injm [prf, in mathcomp.finite_group.morphism]
card_invg [prf, in mathcomp.finite_group.fingroup]
card_irr_pchar [prf, in mathcomp.group_representation.mxrepresentation]
card_iso2 [prf, in mathcomp.solvable.burnside_app]
card_isog [prf, in mathcomp.finite_group.morphism]
card_isog8_extraspecial [prf, in mathcomp.solvable.extraspecial]
card_lcoset [prf, in mathcomp.finite_group.fingroup]
card_lcosets [prf, in mathcomp.finite_group.fingroup]
card_le1_eqP [prf, in mathcomp.boot.fintype]
card_le1_trivg [prf, in mathcomp.finite_group.fingroup]
card_le1P [prf, in mathcomp.boot.fintype]
card_lin_irr [prf, in mathcomp.group_representation.character]
card_linear_irr [prf, in mathcomp.group_representation.mxrepresentation]
card_ltn_sorted_tuples [prf, in mathcomp.boot.binomial]
card_mem_repr [prf, in mathcomp.finite_group.fingroup]
card_modular_group [prf, in mathcomp.solvable.extremal]
card_monic_qpoly [prf, in mathcomp.algebra.qpoly]
card_morphim [prf, in mathcomp.finite_group.quotient]
card_morphpre [prf, in mathcomp.finite_group.quotient]
card_mx [prf, in mathcomp.algebra.matrix]
card_n [prf, in mathcomp.solvable.burnside_app]
card_n2 [prf, in mathcomp.solvable.burnside_app]
card_n2_3 [prf, in mathcomp.solvable.burnside_app]
card_n3 [prf, in mathcomp.solvable.burnside_app]
card_n3_3 [prf, in mathcomp.solvable.burnside_app]
card_n3s [prf, in mathcomp.solvable.burnside_app]
card_n4 [prf, in mathcomp.solvable.burnside_app]
card_npoly [prf, in mathcomp.algebra.qpoly]
card_option [prf, in mathcomp.boot.fintype]
card_orbit [prf, in mathcomp.finite_group.action]
card_orbit1 [prf, in mathcomp.finite_group.action]
card_orbit_in [prf, in mathcomp.finite_group.action]
card_orbit_in_stab [prf, in mathcomp.finite_group.action]
card_orbit_stab [prf, in mathcomp.finite_group.action]
card_ord [prf, in mathcomp.boot.fintype]
card_ord_partitions [prf, in mathcomp.boot.binomial]
card_p1Elem [prf, in mathcomp.solvable.abelian]
card_p1Elem_p2Elem [prf, in mathcomp.solvable.abelian]
card_p1Elem_pnElem [prf, in mathcomp.solvable.abelian]
card_p2group_abelian [prf, in mathcomp.solvable.sylow]
card_p3group_extraspecial [prf, in mathcomp.solvable.maximal]
card_partial_ord_partitions [prf, in mathcomp.boot.binomial]
card_partition [prf, in mathcomp.boot.finset]
card_perm [prf, in mathcomp.finite_group.perm]
card_pfamily [prf, in mathcomp.boot.finfun]
card_pffun_on [prf, in mathcomp.boot.finfun]
card_pgroup [prf, in mathcomp.solvable.pgroup]
card_pnElem [prf, in mathcomp.solvable.abelian]
card_porbit_neq0 [prf, in mathcomp.finite_group.perm]
card_powerset [prf, in mathcomp.boot.finset]
card_pprimeChar [prf, in mathcomp.field.finfield]
card_preim [prf, in mathcomp.boot.fintype]
card_preimset [prf, in mathcomp.boot.finset]
card_primitive_qpoly [prf, in mathcomp.field.qfpoly]
card_prod [prf, in mathcomp.boot.fintype]
card_pX1p2 [prf, in mathcomp.solvable.extraspecial]
card_pX1p2n [prf, in mathcomp.solvable.extraspecial]
card_qfpoly [prf, in mathcomp.field.qfpoly]
card_qfpoly_gt1 [prf, in mathcomp.field.qfpoly]
card_qpoly [prf, in mathcomp.algebra.qpoly]
card_quaternion [prf, in mathcomp.solvable.extremal]
card_quotient [prf, in mathcomp.finite_group.quotient]
card_quotient_subnorm [prf, in mathcomp.finite_group.quotient]
card_rcoset [prf, in mathcomp.finite_group.fingroup]
card_rot [prf, in mathcomp.solvable.burnside_app]
card_rowg [prf, in mathcomp.group_representation.mxabelem]
card_rVabelem [prf, in mathcomp.group_representation.mxabelem]
card_semidihedral [prf, in mathcomp.solvable.extremal]
card_seq_sub [prf, in mathcomp.boot.fintype]
card_setact [prf, in mathcomp.finite_group.action]
card_sig [prf, in mathcomp.boot.fintype]
card_size [prf, in mathcomp.boot.fintype]
card_Sn [prf, in mathcomp.finite_group.perm]
card_sorted_tuples [prf, in mathcomp.boot.binomial]
card_sub [prf, in mathcomp.boot.fintype]
card_subcent1_coset [prf, in mathcomp.group_representation.character]
card_subcent_extraspecial [prf, in mathcomp.solvable.maximal]
card_sum [prf, in mathcomp.boot.fintype]
card_support_normedTI [prf, in mathcomp.solvable.frobenius]
card_Syl [prf, in mathcomp.solvable.sylow]
card_Syl_dvd [prf, in mathcomp.solvable.sylow]
card_Syl_mod [prf, in mathcomp.solvable.sylow]
card_Sym [prf, in mathcomp.solvable.alt]
card_Sym [prf, in mathcomp.finite_group.perm]
card_tagged [prf, in mathcomp.boot.fintype]
card_transversal [prf, in mathcomp.boot.finset]
card_tuple [prf, in mathcomp.boot.tuple]
card_uniform_partition [prf, in mathcomp.boot.finset]
card_uniq_tuple [prf, in mathcomp.solvable.primitive_action]
card_uniq_tuples [prf, in mathcomp.boot.binomial]
card_uniqP [prf, in mathcomp.boot.fintype]
card_unit [prf, in mathcomp.boot.fintype]
card_units_Zp [prf, in mathcomp.algebra.zmodp]
card_void [prf, in mathcomp.boot.fintype]
card_vspace [prf, in mathcomp.field.finfield]
card_vspace1 [prf, in mathcomp.field.finfield]
card_vspacef [prf, in mathcomp.field.finfield]
card_Zp [prf, in mathcomp.algebra.zmodp]
cardC [prf, in mathcomp.boot.fintype]
cardC1 [prf, in mathcomp.boot.fintype]
cardD1 [prf, in mathcomp.boot.fintype]
cardD1x [prf, in mathcomp.boot.bigop]
cardE [prf, in mathcomp.boot.fintype]
cardG_gt0 [prf, in mathcomp.finite_group.fingroup]
cardG_gt1 [prf, in mathcomp.finite_group.fingroup]
cardID [prf, in mathcomp.boot.fintype]
cardIg_divn [prf, in mathcomp.finite_group.fingroup]
cardJg [prf, in mathcomp.finite_group.fingroup]
cardMg_divn [prf, in mathcomp.finite_group.fingroup]
cardMg_TI [prf, in mathcomp.finite_group.fingroup]
cards0 [prf, in mathcomp.boot.finset]
cards0_eq [prf, in mathcomp.boot.finset]
cards1 [prf, in mathcomp.boot.finset]
cards1P [prf, in mathcomp.boot.finset]
cards2 [prf, in mathcomp.boot.finset]
cards2P [prf, in mathcomp.boot.finset]
cards_draws [prf, in mathcomp.boot.binomial]
cards_eq0 [prf, in mathcomp.boot.finset]
cards_eqP [prf, in mathcomp.boot.finset]
cardsC [prf, in mathcomp.boot.finset]
cardsC1 [prf, in mathcomp.boot.finset]
cardsCs [prf, in mathcomp.boot.finset]
cardsD [prf, in mathcomp.boot.finset]
cardsD1 [prf, in mathcomp.boot.finset]
cardsDS [prf, in mathcomp.boot.finset]
cardsE [prf, in mathcomp.boot.finset]
cardSg [prf, in mathcomp.finite_group.fingroup]
cardSg_cyclic [prf, in mathcomp.solvable.cyclic]
cardsI [prf, in mathcomp.boot.finset]
cardsID [prf, in mathcomp.boot.finset]
cardsT [prf, in mathcomp.boot.finset]
cardsU [prf, in mathcomp.boot.finset]
cardsU1 [prf, in mathcomp.boot.finset]
cardsUI [prf, in mathcomp.boot.finset]
cardsX [prf, in mathcomp.boot.finset]
cardsXn [prf, in mathcomp.boot.finset]
cardT [prf, in mathcomp.boot.fintype]
cardU1 [prf, in mathcomp.boot.fintype]
cardUI [prf, in mathcomp.boot.fintype]
cardX [prf, in mathcomp.boot.fintype]
cast_bseq_id [prf, in mathcomp.boot.tuple]
cast_bseq_trans [prf, in mathcomp.boot.tuple]
cast_bseqEwiden [prf, in mathcomp.boot.tuple]
cast_bseqK [prf, in mathcomp.boot.tuple]
cast_bseqKV [prf, in mathcomp.boot.tuple]
cast_col_mx [prf, in mathcomp.algebra.matrix]
cast_ord_comp [prf, in mathcomp.boot.fintype]
cast_ord_id [prf, in mathcomp.boot.fintype]
cast_ord_inj [prf, in mathcomp.boot.fintype]
cast_ord_permE [prf, in mathcomp.finite_group.perm]
cast_ord_proof [prf, in mathcomp.boot.fintype]
cast_ordK [prf, in mathcomp.boot.fintype]
cast_ordKV [prf, in mathcomp.boot.fintype]
cast_perm_comp [prf, in mathcomp.finite_group.perm]
cast_perm_id [prf, in mathcomp.finite_group.perm]
cast_perm_inj [prf, in mathcomp.finite_group.perm]
cast_perm_morphM [prf, in mathcomp.finite_group.perm]
cast_perm_sym [prf, in mathcomp.finite_group.perm]
cast_permE [prf, in mathcomp.finite_group.perm]
cast_permK [prf, in mathcomp.finite_group.perm]
cast_permKV [prf, in mathcomp.finite_group.perm]
cast_row_mx [prf, in mathcomp.algebra.matrix]
castmx_comp [prf, in mathcomp.algebra.matrix]
castmx_const [prf, in mathcomp.algebra.matrix]
castmx_id [prf, in mathcomp.algebra.matrix]
castmx_sym [prf, in mathcomp.algebra.matrix]
castmxE [prf, in mathcomp.algebra.matrix]
castmxEsub [prf, in mathcomp.algebra.matrix]
castmxK [prf, in mathcomp.algebra.matrix]
castmxKV [prf, in mathcomp.algebra.matrix]
castt_comp [prf, in mathcomp.algebra.tensor]
castt_id [prf, in mathcomp.algebra.tensor]
casttK [prf, in mathcomp.algebra.tensor]
casttKV [prf, in mathcomp.algebra.tensor]
cat0s [prf, in mathcomp.boot.seq]
cat1s [prf, in mathcomp.boot.seq]
cat_basis [prf, in mathcomp.algebra.vector]
cat_bseqP [prf, in mathcomp.boot.tuple]
cat_cons [prf, in mathcomp.boot.seq]
cat_free [prf, in mathcomp.algebra.vector]
cat_inl [prf, in mathcomp.boot.finfun]
cat_inr [prf, in mathcomp.boot.finfun]
cat_lshift [prf, in mathcomp.boot.finfun]
cat_nilp [prf, in mathcomp.boot.seq]
cat_nseq [prf, in mathcomp.boot.seq]
cat_ordfun_comp [prf, in mathcomp.boot.finfun]
cat_ordfunK [prf, in mathcomp.boot.finfun]
cat_path [prf, in mathcomp.boot.path]
cat_rcons [prf, in mathcomp.boot.seq]
cat_rshift [prf, in mathcomp.boot.finfun]
cat_sorted2 [prf, in mathcomp.boot.path]
cat_subseq [prf, in mathcomp.boot.seq]
cat_take_drop [prf, in mathcomp.boot.seq]
cat_tupleP [prf, in mathcomp.boot.tuple]
cat_uniq [prf, in mathcomp.boot.seq]
catA [prf, in mathcomp.boot.seq]
catCA_perm_ind [prf, in mathcomp.boot.seq]
catCA_perm_subst [prf, in mathcomp.boot.seq]
catl2_infix [prf, in mathcomp.boot.seq]
catl_free [prf, in mathcomp.algebra.vector]
catl_infix [prf, in mathcomp.boot.seq]
catl_prefix [prf, in mathcomp.boot.seq]
catl_suffix [prf, in mathcomp.boot.seq]
catr2_infix [prf, in mathcomp.boot.seq]
catr_free [prf, in mathcomp.algebra.vector]
catr_infix [prf, in mathcomp.boot.seq]
catrev_catl [prf, in mathcomp.boot.seq]
catrev_catr [prf, in mathcomp.boot.seq]
catrevE [prf, in mathcomp.boot.seq]
cats0 [prf, in mathcomp.boot.seq]
cats1 [prf, in mathcomp.boot.seq]
Cauchy [prf, in mathcomp.solvable.pgroup]
CauchySchwarz [prf, in mathcomp.algebra.sesquilinear]
CauchySchwarz_sqrt [prf, in mathcomp.algebra.sesquilinear]
Cayley_Hamilton [prf, in mathcomp.algebra.mxpoly]
Cayley_isog [prf, in mathcomp.finite_group.action]
Cayley_isom [prf, in mathcomp.finite_group.action]
ceil_rat [prf, in mathcomp.algebra.rat]
ceilErat [prf, in mathcomp.algebra.rat]
cent11T [prf, in mathcomp.finite_group.fingroup]
cent1_extraspecial_maximal [prf, in mathcomp.solvable.maximal]
cent1_normedTI [prf, in mathcomp.solvable.frobenius]
cent1C [prf, in mathcomp.finite_group.fingroup]
cent1E [prf, in mathcomp.finite_group.fingroup]
cent1id [prf, in mathcomp.finite_group.fingroup]
cent1J [prf, in mathcomp.finite_group.fingroup]
cent1P [prf, in mathcomp.finite_group.fingroup]
cent1T [prf, in mathcomp.finite_group.fingroup]
cent1v1 [prf, in mathcomp.field.falgebra]
cent1v_id [prf, in mathcomp.field.falgebra]
cent1vC [prf, in mathcomp.field.falgebra]
cent1vP [prf, in mathcomp.field.falgebra]
cent1vX [prf, in mathcomp.field.falgebra]
cent_centerv [prf, in mathcomp.field.falgebra]
cent_classP [prf, in mathcomp.finite_group.fingroup]
cent_cycle [prf, in mathcomp.finite_group.fingroup]
cent_gen [prf, in mathcomp.finite_group.fingroup]
cent_joinEl [prf, in mathcomp.finite_group.fingroup]
cent_joinEr [prf, in mathcomp.finite_group.fingroup]
cent_mx_fun_is_linear [prf, in mathcomp.algebra.mxalgebra]
cent_mx_ideal [prf, in mathcomp.algebra.mxalgebra]
cent_mx_ring [prf, in mathcomp.algebra.mxalgebra]
cent_mx_scalar_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
cent_mxP [prf, in mathcomp.algebra.mxalgebra]
cent_norm [prf, in mathcomp.finite_group.fingroup]
cent_normal [prf, in mathcomp.finite_group.fingroup]
cent_rowP [prf, in mathcomp.algebra.mxalgebra]
cent_semiprime [prf, in mathcomp.solvable.frobenius]
cent_semiregular [prf, in mathcomp.solvable.frobenius]
cent_set1 [prf, in mathcomp.finite_group.fingroup]
cent_sub [prf, in mathcomp.finite_group.fingroup]
cent_sub_Inertia [prf, in mathcomp.group_representation.inertia]
cent_sub_inertia [prf, in mathcomp.group_representation.inertia]
centC [prf, in mathcomp.finite_group.fingroup]
center1 [prf, in mathcomp.solvable.center]
center_abelian [prf, in mathcomp.solvable.center]
center_aut_extraspecial [prf, in mathcomp.solvable.maximal]
center_bigcprod [prf, in mathcomp.solvable.center]
center_bigdprod [prf, in mathcomp.solvable.center]
center_char [prf, in mathcomp.solvable.center]
center_class_formula [prf, in mathcomp.solvable.center]
center_cprod [prf, in mathcomp.solvable.center]
center_dprod [prf, in mathcomp.solvable.center]
center_idP [prf, in mathcomp.solvable.center]
center_kquo_cyclic [prf, in mathcomp.group_representation.mxrepresentation]
center_mx_sub [prf, in mathcomp.algebra.mxalgebra]
center_mxP [prf, in mathcomp.algebra.mxalgebra]
center_ncprod [prf, in mathcomp.solvable.center]
center_ncprod0 [prf, in mathcomp.solvable.center]
center_nil_eq1 [prf, in mathcomp.solvable.nilpotent]
center_normal [prf, in mathcomp.solvable.center]
center_prod [prf, in mathcomp.solvable.center]
center_special_abelem [prf, in mathcomp.solvable.maximal]
center_sub [prf, in mathcomp.solvable.center]
center_sub_Inertia [prf, in mathcomp.group_representation.inertia]
centerC [prf, in mathcomp.solvable.center]
centerP [prf, in mathcomp.solvable.center]
centerv_sub [prf, in mathcomp.field.falgebra]
centgmx_hom [prf, in mathcomp.group_representation.mxrepresentation]
centgmx_map [prf, in mathcomp.group_representation.mxrepresentation]
centgmxP [prf, in mathcomp.group_representation.mxrepresentation]
centI [prf, in mathcomp.finite_group.fingroup]
centJ [prf, in mathcomp.finite_group.fingroup]
centM [prf, in mathcomp.finite_group.fingroup]
centP [prf, in mathcomp.finite_group.fingroup]
central_central_factor [prf, in mathcomp.solvable.gseries]
central_factor_central [prf, in mathcomp.solvable.gseries]
centraliser1_is_aspace [prf, in mathcomp.field.falgebra]
centraliser_is_aspace [prf, in mathcomp.field.falgebra]
centrals_nil [prf, in mathcomp.solvable.nilpotent]
centS [prf, in mathcomp.finite_group.fingroup]
cents1 [prf, in mathcomp.finite_group.fingroup]
cents_cycle [prf, in mathcomp.finite_group.fingroup]
cents_norm [prf, in mathcomp.finite_group.fingroup]
centsC [prf, in mathcomp.finite_group.fingroup]
centsP [prf, in mathcomp.finite_group.fingroup]
centSS [prf, in mathcomp.finite_group.fingroup]
centsS [prf, in mathcomp.finite_group.fingroup]
centU [prf, in mathcomp.finite_group.fingroup]
centv1 [prf, in mathcomp.field.falgebra]
centv_algid [prf, in mathcomp.field.falgebra]
centvC [prf, in mathcomp.field.falgebra]
centvP [prf, in mathcomp.field.falgebra]
centvsP [prf, in mathcomp.field.falgebra]
centvX [prf, in mathcomp.field.falgebra]
centY [prf, in mathcomp.finite_group.fingroup]
cf_triangle_leif [prf, in mathcomp.group_representation.classfun]
cfaithful_quo [prf, in mathcomp.group_representation.classfun]
cfaithful_reg [prf, in mathcomp.group_representation.character]
cfaithfulE [prf, in mathcomp.group_representation.classfun]
cfAut_cfun1 [prf, in mathcomp.group_representation.classfun]
cfAut_cfun1i [prf, in mathcomp.group_representation.classfun]
cfAut_cfuni [prf, in mathcomp.group_representation.classfun]
cfAut_char [prf, in mathcomp.group_representation.character]
cfAut_char1 [prf, in mathcomp.group_representation.character]
cfAut_eq1 [prf, in mathcomp.group_representation.classfun]
cfAut_inj [prf, in mathcomp.group_representation.classfun]
cfAut_irr [prf, in mathcomp.group_representation.character]
cfAut_irr1 [prf, in mathcomp.group_representation.character]
cfAut_is_monoid_morphism [prf, in mathcomp.group_representation.classfun]
cfAut_is_zmod_morphism [prf, in mathcomp.group_representation.classfun]
cfAut_lin_char [prf, in mathcomp.group_representation.character]
cfAut_on [prf, in mathcomp.group_representation.classfun]
cfAut_scalable [prf, in mathcomp.group_representation.classfun]
cfAut_vchar [prf, in mathcomp.group_representation.vcharacter]
cfAut_zchar [prf, in mathcomp.group_representation.vcharacter]
cfAutConjg [prf, in mathcomp.group_representation.inertia]
cfAutDprod [prf, in mathcomp.group_representation.classfun]
cfAutDprodl [prf, in mathcomp.group_representation.classfun]
cfAutDprodr [prf, in mathcomp.group_representation.classfun]
cfAutInd [prf, in mathcomp.group_representation.classfun]
cfAutIsom [prf, in mathcomp.group_representation.classfun]
cfAutK [prf, in mathcomp.group_representation.classfun]
cfAutMod [prf, in mathcomp.group_representation.classfun]
cfAutMorph [prf, in mathcomp.group_representation.classfun]
cfAutQuo [prf, in mathcomp.group_representation.classfun]
cfAutRes [prf, in mathcomp.group_representation.classfun]
cfAutVK [prf, in mathcomp.group_representation.classfun]
cfAutZ [prf, in mathcomp.group_representation.classfun]
cfAutZ_Cint [prf, in mathcomp.group_representation.classfun]
cfAutZ_Cnat [prf, in mathcomp.group_representation.classfun]
cfAutZ_nat [prf, in mathcomp.group_representation.classfun]
cfBigdprod1 [prf, in mathcomp.group_representation.classfun]
cfBigdprod_char [prf, in mathcomp.group_representation.character]
cfBigdprod_eq1 [prf, in mathcomp.group_representation.character]
cfBigdprod_irr [prf, in mathcomp.group_representation.character]
cfBigdprod_lin_char [prf, in mathcomp.group_representation.character]
cfBigdprod_Res_lin [prf, in mathcomp.group_representation.character]
cfBigdprodE [prf, in mathcomp.group_representation.classfun]
cfBigdprodEi [prf, in mathcomp.group_representation.classfun]
cfBigdprodi1 [prf, in mathcomp.group_representation.classfun]
cfBigdprodi_char [prf, in mathcomp.group_representation.character]
cfBigdprodi_charE [prf, in mathcomp.group_representation.character]
cfBigdprodi_eq1 [prf, in mathcomp.group_representation.classfun]
cfBigdprodi_inj [prf, in mathcomp.group_representation.classfun]
cfBigdprodi_irr [prf, in mathcomp.group_representation.character]
cfBigdprodi_iso [prf, in mathcomp.group_representation.classfun]
cfBigdprodi_lin_char [prf, in mathcomp.group_representation.character]
cfBigdprodi_lin_charE [prf, in mathcomp.group_representation.character]
cfBigdprodiK [prf, in mathcomp.group_representation.classfun]
cfBigdprodK [prf, in mathcomp.group_representation.classfun]
cfBigdprodKabelian [prf, in mathcomp.group_representation.character]
cfBigdprodKlin [prf, in mathcomp.group_representation.character]
cfCauchySchwarz [prf, in mathcomp.group_representation.classfun]
cfCauchySchwarz_sqrt [prf, in mathcomp.group_representation.classfun]
cfcenter_cyclic [prf, in mathcomp.group_representation.character]
cfcenter_eq_center [prf, in mathcomp.group_representation.character]
cfcenter_fful_irr [prf, in mathcomp.group_representation.character]
cfcenter_group_set [prf, in mathcomp.group_representation.character]
cfcenter_normal [prf, in mathcomp.group_representation.character]
cfcenter_repr [prf, in mathcomp.group_representation.character]
cfcenter_Res [prf, in mathcomp.group_representation.character]
cfcenter_sub [prf, in mathcomp.group_representation.character]
cfcenter_subset_center [prf, in mathcomp.group_representation.character]
cfclass1 [prf, in mathcomp.group_representation.inertia]
cfclass_IirrE [prf, in mathcomp.group_representation.inertia]
cfclass_Ind [prf, in mathcomp.group_representation.inertia]
cfclass_inertia [prf, in mathcomp.group_representation.inertia]
cfclass_invariant [prf, in mathcomp.group_representation.inertia]
cfclass_refl [prf, in mathcomp.group_representation.inertia]
cfclass_sym [prf, in mathcomp.group_representation.inertia]
cfclass_transr [prf, in mathcomp.group_representation.inertia]
cfclass_uniq [prf, in mathcomp.group_representation.inertia]
cfclassInorm [prf, in mathcomp.group_representation.inertia]
cfclassP [prf, in mathcomp.group_representation.inertia]
cfConjC_cfun1 [prf, in mathcomp.group_representation.classfun]
cfConjC_char [prf, in mathcomp.group_representation.character]
cfConjC_char1 [prf, in mathcomp.group_representation.character]
cfConjC_irr [prf, in mathcomp.group_representation.character]
cfConjC_irr1 [prf, in mathcomp.group_representation.character]
cfConjC_lin_char [prf, in mathcomp.group_representation.character]
cfConjCE [prf, in mathcomp.group_representation.classfun]
cfConjCK [prf, in mathcomp.group_representation.classfun]
cfConjg1 [prf, in mathcomp.group_representation.inertia]
cfConjg_cfun1 [prf, in mathcomp.group_representation.inertia]
cfConjg_cfuni [prf, in mathcomp.group_representation.inertia]
cfConjg_cfuniJ [prf, in mathcomp.group_representation.inertia]
cfConjg_char [prf, in mathcomp.group_representation.inertia]
cfConjg_eq1 [prf, in mathcomp.group_representation.inertia]
cfConjg_eqE [prf, in mathcomp.group_representation.inertia]
cfConjg_id [prf, in mathcomp.group_representation.inertia]
cfConjg_irr [prf, in mathcomp.group_representation.inertia]
cfConjg_is_linear [prf, in mathcomp.group_representation.inertia]
cfConjg_is_monoid_morphism [prf, in mathcomp.group_representation.inertia]
cfConjg_iso [prf, in mathcomp.group_representation.inertia]
cfConjg_lin_char [prf, in mathcomp.group_representation.inertia]
cfConjgBigdprod [prf, in mathcomp.group_representation.inertia]
cfConjgBigdprodi [prf, in mathcomp.group_representation.inertia]
cfConjgDprod [prf, in mathcomp.group_representation.inertia]
cfConjgDprodl [prf, in mathcomp.group_representation.inertia]
cfConjgDprodr [prf, in mathcomp.group_representation.inertia]
cfConjgE [prf, in mathcomp.group_representation.inertia]
cfConjgEin [prf, in mathcomp.group_representation.inertia]
cfConjgEJ [prf, in mathcomp.group_representation.inertia]
cfConjgEout [prf, in mathcomp.group_representation.inertia]
cfConjgInd [prf, in mathcomp.group_representation.inertia]
cfConjgInd_norm [prf, in mathcomp.group_representation.inertia]
cfConjgIsom [prf, in mathcomp.group_representation.inertia]
cfConjgJ1 [prf, in mathcomp.group_representation.inertia]
cfConjgK [prf, in mathcomp.group_representation.inertia]
cfConjgKV [prf, in mathcomp.group_representation.inertia]
cfConjgM [prf, in mathcomp.group_representation.inertia]
cfConjgMnorm [prf, in mathcomp.group_representation.inertia]
cfConjgMod [prf, in mathcomp.group_representation.inertia]
cfConjgMod_norm [prf, in mathcomp.group_representation.inertia]
cfConjgMorph [prf, in mathcomp.group_representation.inertia]
cfConjgQuo [prf, in mathcomp.group_representation.inertia]
cfConjgQuo_norm [prf, in mathcomp.group_representation.inertia]
cfConjgRes [prf, in mathcomp.group_representation.inertia]
cfConjgRes_norm [prf, in mathcomp.group_representation.inertia]
cfConjgSdprod [prf, in mathcomp.group_representation.inertia]
cfDet0 [prf, in mathcomp.group_representation.character]
cfDet_id [prf, in mathcomp.group_representation.character]
cfDet_lin_char [prf, in mathcomp.group_representation.character]
cfDet_mul_lin [prf, in mathcomp.group_representation.character]
cfDetConjg [prf, in mathcomp.group_representation.inertia]
cfDetD [prf, in mathcomp.group_representation.character]
cfDetIsom [prf, in mathcomp.group_representation.character]
cfDetMn [prf, in mathcomp.group_representation.character]
cfDetMorph [prf, in mathcomp.group_representation.character]
cfDetRepr [prf, in mathcomp.group_representation.character]
cfDetRes [prf, in mathcomp.group_representation.character]
cfdot0l [prf, in mathcomp.group_representation.classfun]
cfdot0r [prf, in mathcomp.group_representation.classfun]
cfdot_add_dirr_eq1 [prf, in mathcomp.group_representation.vcharacter]
cfdot_aut_char [prf, in mathcomp.group_representation.character]
cfdot_aut_irr [prf, in mathcomp.group_representation.character]
cfdot_aut_vchar [prf, in mathcomp.group_representation.vcharacter]
cfdot_bigdprod [prf, in mathcomp.group_representation.classfun]
cfdot_cfAut [prf, in mathcomp.group_representation.classfun]
cfdot_cfuni [prf, in mathcomp.group_representation.classfun]
cfdot_char_r [prf, in mathcomp.group_representation.character]
cfdot_complement [prf, in mathcomp.group_representation.classfun]
cfdot_conjC [prf, in mathcomp.group_representation.classfun]
cfdot_conjCl [prf, in mathcomp.group_representation.classfun]
cfdot_conjCr [prf, in mathcomp.group_representation.classfun]
cfdot_dchi [prf, in mathcomp.group_representation.vcharacter]
cfdot_dirr [prf, in mathcomp.group_representation.vcharacter]
cfdot_dirr_eq1 [prf, in mathcomp.group_representation.vcharacter]
cfdot_dprod [prf, in mathcomp.group_representation.classfun]
cfdot_dprod_irr [prf, in mathcomp.group_representation.character]
cfdot_irr [prf, in mathcomp.group_representation.character]
cfdot_irr_conjg [prf, in mathcomp.group_representation.inertia]
cfdot_real_conjC [prf, in mathcomp.group_representation.classfun]
cfdot_Res_conjg [prf, in mathcomp.group_representation.inertia]
cfdot_Res_ge_constt [prf, in mathcomp.group_representation.character]
cfdot_Res_l [prf, in mathcomp.group_representation.classfun]
cfdot_sum_dchi [prf, in mathcomp.group_representation.vcharacter]
cfdot_sum_irr [prf, in mathcomp.group_representation.character]
cfdot_sum_orthogonal [prf, in mathcomp.group_representation.vcharacter]
cfdot_sum_orthonormal [prf, in mathcomp.group_representation.vcharacter]
cfdot_suml [prf, in mathcomp.group_representation.classfun]
cfdot_sumr [prf, in mathcomp.group_representation.classfun]
cfdot_todirrE [prf, in mathcomp.group_representation.vcharacter]
cfdot_vchar_r [prf, in mathcomp.group_representation.vcharacter]
cfdotBl [prf, in mathcomp.group_representation.classfun]
cfdotBr [prf, in mathcomp.group_representation.classfun]
cfdotC [prf, in mathcomp.group_representation.classfun]
cfdotC_char [prf, in mathcomp.group_representation.character]
cfdotDl [prf, in mathcomp.group_representation.classfun]
cfdotDr [prf, in mathcomp.group_representation.classfun]
cfdotE [prf, in mathcomp.group_representation.classfun]
cfdotEl [prf, in mathcomp.group_representation.classfun]
cfdotElr [prf, in mathcomp.group_representation.classfun]
cfdotEr [prf, in mathcomp.group_representation.classfun]
cfdotMnl [prf, in mathcomp.group_representation.classfun]
cfdotMnr [prf, in mathcomp.group_representation.classfun]
cfdotNl [prf, in mathcomp.group_representation.classfun]
cfdotNr [prf, in mathcomp.group_representation.classfun]
cfdotr_is_linear [prf, in mathcomp.group_representation.classfun]
cfdotrE [prf, in mathcomp.group_representation.classfun]
cfdotZl [prf, in mathcomp.group_representation.classfun]
cfdotZr [prf, in mathcomp.group_representation.classfun]
cfDprod1 [prf, in mathcomp.group_representation.classfun]
cfDprod_cfun1 [prf, in mathcomp.group_representation.classfun]
cfDprod_cfun1l [prf, in mathcomp.group_representation.classfun]
cfDprod_cfun1r [prf, in mathcomp.group_representation.classfun]
cfDprod_char [prf, in mathcomp.group_representation.character]
cfDprod_eq1 [prf, in mathcomp.group_representation.character]
cfDprod_irr [prf, in mathcomp.group_representation.character]
cfDprod_lin_char [prf, in mathcomp.group_representation.character]
cfDprod_Resl [prf, in mathcomp.group_representation.classfun]
cfDprod_Resr [prf, in mathcomp.group_representation.classfun]
cfDprod_split [prf, in mathcomp.group_representation.classfun]
cfDprodC [prf, in mathcomp.group_representation.classfun]
cfDprodE [prf, in mathcomp.group_representation.classfun]
cfDprodEl [prf, in mathcomp.group_representation.classfun]
cfDprodEr [prf, in mathcomp.group_representation.classfun]
cfDprodKl [prf, in mathcomp.group_representation.classfun]
cfDprodKl_abelian [prf, in mathcomp.group_representation.character]
cfDprodKr [prf, in mathcomp.group_representation.classfun]
cfDprodKr_abelian [prf, in mathcomp.group_representation.character]
cfDprodl1 [prf, in mathcomp.group_representation.classfun]
cfDprodl_char [prf, in mathcomp.group_representation.character]
cfDprodl_eq1 [prf, in mathcomp.group_representation.classfun]
cfDprodl_irr [prf, in mathcomp.group_representation.character]
cfDprodl_iso [prf, in mathcomp.group_representation.classfun]
cfDprodl_lin_char [prf, in mathcomp.group_representation.character]
cfDprodlK [prf, in mathcomp.group_representation.classfun]
cfDprodr1 [prf, in mathcomp.group_representation.classfun]
cfDprodr_char [prf, in mathcomp.group_representation.character]
cfDprodr_eq1 [prf, in mathcomp.group_representation.classfun]
cfDprodr_irr [prf, in mathcomp.group_representation.character]
cfDprodr_iso [prf, in mathcomp.group_representation.classfun]
cfDprodr_lin_char [prf, in mathcomp.group_representation.character]
cfDprodrK [prf, in mathcomp.group_representation.classfun]
cfExp_prime_transitive [prf, in mathcomp.group_representation.character]
cfIirr_key [prf, in mathcomp.group_representation.character]
cfIirrE [prf, in mathcomp.group_representation.character]
cfIirrPE [prf, in mathcomp.group_representation.character]
cfInd1 [prf, in mathcomp.group_representation.classfun]
cfInd_cfun1 [prf, in mathcomp.group_representation.classfun]
cfInd_char [prf, in mathcomp.group_representation.character]
cfInd_eq0 [prf, in mathcomp.group_representation.character]
cfInd_id [prf, in mathcomp.group_representation.classfun]
cfInd_is_linear [prf, in mathcomp.group_representation.classfun]
cfInd_normal [prf, in mathcomp.group_representation.classfun]
cfInd_on [prf, in mathcomp.group_representation.classfun]
cfInd_vchar [prf, in mathcomp.group_representation.vcharacter]
cfIndE [prf, in mathcomp.group_representation.classfun]
cfIndEout [prf, in mathcomp.group_representation.classfun]
cfIndEsdprod [prf, in mathcomp.group_representation.classfun]
cfIndInd [prf, in mathcomp.group_representation.classfun]
cfIndIsom [prf, in mathcomp.group_representation.classfun]
cfIndM [prf, in mathcomp.group_representation.classfun]
cfIndMorph [prf, in mathcomp.group_representation.classfun]
cfIsom1 [prf, in mathcomp.group_representation.classfun]
cfIsom_cfun1 [prf, in mathcomp.group_representation.classfun]
cfIsom_char [prf, in mathcomp.group_representation.character]
cfIsom_eq1 [prf, in mathcomp.group_representation.classfun]
cfIsom_inj [prf, in mathcomp.group_representation.classfun]
cfIsom_irr [prf, in mathcomp.group_representation.character]
cfIsom_is_monoid_morphism [prf, in mathcomp.group_representation.classfun]
cfIsom_is_scalable [prf, in mathcomp.group_representation.classfun]
cfIsom_is_zmod_morphism [prf, in mathcomp.group_representation.classfun]
cfIsom_iso [prf, in mathcomp.group_representation.classfun]
cfIsom_key [prf, in mathcomp.group_representation.classfun]
cfIsom_lin_char [prf, in mathcomp.group_representation.character]
cfIsomE [prf, in mathcomp.group_representation.classfun]
cfIsomK [prf, in mathcomp.group_representation.classfun]
cfIsomKV [prf, in mathcomp.group_representation.classfun]
cfker1 [prf, in mathcomp.group_representation.classfun]
cfker_add [prf, in mathcomp.group_representation.classfun]
cfker_aut [prf, in mathcomp.group_representation.classfun]
cfker_center_normal [prf, in mathcomp.group_representation.character]
cfker_cfun0 [prf, in mathcomp.group_representation.classfun]
cfker_cfun1 [prf, in mathcomp.group_representation.classfun]
cfker_conjg [prf, in mathcomp.group_representation.inertia]
cfker_constt [prf, in mathcomp.group_representation.character]
cfker_dprod [prf, in mathcomp.group_representation.classfun]
cfker_dprodl [prf, in mathcomp.group_representation.classfun]
cfker_dprodr [prf, in mathcomp.group_representation.classfun]
cfker_Ind [prf, in mathcomp.group_representation.character]
cfker_Ind_irr [prf, in mathcomp.group_representation.character]
cfker_irr0 [prf, in mathcomp.group_representation.character]
cfker_is_group [prf, in mathcomp.group_representation.classfun]
cfker_isom [prf, in mathcomp.group_representation.classfun]
cfker_mod [prf, in mathcomp.group_representation.classfun]
cfker_morph [prf, in mathcomp.group_representation.classfun]
cfker_morph_im [prf, in mathcomp.group_representation.classfun]
cfker_mul [prf, in mathcomp.group_representation.classfun]
cfker_norm [prf, in mathcomp.group_representation.classfun]
cfker_normal [prf, in mathcomp.group_representation.classfun]
cfker_nzcharE [prf, in mathcomp.group_representation.character]
cfker_opp [prf, in mathcomp.group_representation.classfun]
cfker_prod [prf, in mathcomp.group_representation.classfun]
cfker_quo [prf, in mathcomp.group_representation.classfun]
cfker_reg_quo [prf, in mathcomp.group_representation.character]
cfker_repr [prf, in mathcomp.group_representation.character]
cfker_Res [prf, in mathcomp.group_representation.character]
cfker_scale [prf, in mathcomp.group_representation.classfun]
cfker_scale_nz [prf, in mathcomp.group_representation.classfun]
cfker_sdprod [prf, in mathcomp.group_representation.classfun]
cfker_sub [prf, in mathcomp.group_representation.classfun]
cfker_sum [prf, in mathcomp.group_representation.classfun]
cfkerE [prf, in mathcomp.group_representation.character]
cfkerEchar [prf, in mathcomp.group_representation.character]
cfkerEirr [prf, in mathcomp.group_representation.character]
cfkerMl [prf, in mathcomp.group_representation.classfun]
cfkerMr [prf, in mathcomp.group_representation.classfun]
cfMod1 [prf, in mathcomp.group_representation.classfun]
cfMod_cfun1 [prf, in mathcomp.group_representation.classfun]
cfMod_char [prf, in mathcomp.group_representation.character]
cfMod_charE [prf, in mathcomp.group_representation.character]
cfMod_eq1 [prf, in mathcomp.group_representation.classfun]
cfMod_irr [prf, in mathcomp.group_representation.character]
cfMod_iso [prf, in mathcomp.group_representation.classfun]
cfMod_lin_char [prf, in mathcomp.group_representation.character]
cfMod_lin_charE [prf, in mathcomp.group_representation.character]
cfModE [prf, in mathcomp.group_representation.classfun]
cfModK [prf, in mathcomp.group_representation.classfun]
cfMorph1 [prf, in mathcomp.group_representation.classfun]
cfMorph_cfun1 [prf, in mathcomp.group_representation.classfun]
cfMorph_char [prf, in mathcomp.group_representation.character]
cfMorph_charE [prf, in mathcomp.group_representation.character]
cfMorph_eq1 [prf, in mathcomp.group_representation.classfun]
cfMorph_inj [prf, in mathcomp.group_representation.classfun]
cfMorph_irr [prf, in mathcomp.group_representation.character]
cfMorph_is_linear [prf, in mathcomp.group_representation.classfun]
cfMorph_is_monoid_morphism [prf, in mathcomp.group_representation.classfun]
cfMorph_iso [prf, in mathcomp.group_representation.classfun]
cfMorph_lin_char [prf, in mathcomp.group_representation.character]
cfMorph_lin_charE [prf, in mathcomp.group_representation.character]
cfMorphE [prf, in mathcomp.group_representation.classfun]
cfMorphEout [prf, in mathcomp.group_representation.classfun]
cfnorm1 [prf, in mathcomp.group_representation.classfun]
cfnorm_conjC [prf, in mathcomp.group_representation.classfun]
cfnorm_dchi [prf, in mathcomp.group_representation.vcharacter]
cfnorm_eq0 [prf, in mathcomp.group_representation.classfun]
cfnorm_ge0 [prf, in mathcomp.group_representation.classfun]
cfnorm_gt0 [prf, in mathcomp.group_representation.classfun]
cfnorm_Ind_cfun1 [prf, in mathcomp.group_representation.classfun]
cfnorm_irr [prf, in mathcomp.group_representation.character]
cfnorm_map_orthonormal [prf, in mathcomp.group_representation.vcharacter]
cfnorm_orthogonal [prf, in mathcomp.group_representation.vcharacter]
cfnorm_orthonormal [prf, in mathcomp.group_representation.vcharacter]
cfnorm_quo [prf, in mathcomp.group_representation.classfun]
cfnorm_Res_leif [prf, in mathcomp.group_representation.character]
cfnorm_sign [prf, in mathcomp.group_representation.classfun]
cfnorm_sum_orthogonal [prf, in mathcomp.group_representation.vcharacter]
cfnorm_sum_orthonormal [prf, in mathcomp.group_representation.vcharacter]
cfnormB [prf, in mathcomp.group_representation.classfun]
cfnormBd [prf, in mathcomp.group_representation.classfun]
cfnormD [prf, in mathcomp.group_representation.classfun]
cfnormDd [prf, in mathcomp.group_representation.classfun]
cfnormE [prf, in mathcomp.group_representation.classfun]
cfnormN [prf, in mathcomp.group_representation.classfun]
cfnormZ [prf, in mathcomp.group_representation.classfun]
cforder_aut [prf, in mathcomp.group_representation.classfun]
cforder_dprodl [prf, in mathcomp.group_representation.classfun]
cforder_dprodr [prf, in mathcomp.group_representation.classfun]
cforder_inj_rmorph [prf, in mathcomp.group_representation.classfun]
cforder_irr_eq1 [prf, in mathcomp.group_representation.character]
cforder_isom [prf, in mathcomp.group_representation.classfun]
cforder_lin_char [prf, in mathcomp.group_representation.character]
cforder_lin_char_dvdG [prf, in mathcomp.group_representation.character]
cforder_lin_char_gt0 [prf, in mathcomp.group_representation.character]
cforder_mod [prf, in mathcomp.group_representation.classfun]
cforder_morph [prf, in mathcomp.group_representation.classfun]
cforder_quo [prf, in mathcomp.group_representation.classfun]
cforder_Res [prf, in mathcomp.group_representation.classfun]
cforder_rmorph [prf, in mathcomp.group_representation.classfun]
cforder_sdprod [prf, in mathcomp.group_representation.classfun]
cfproj_sum_orthogonal [prf, in mathcomp.group_representation.vcharacter]
cfproj_sum_orthonormal [prf, in mathcomp.group_representation.vcharacter]
cfQuo1 [prf, in mathcomp.group_representation.classfun]
cfQuo_cfun1 [prf, in mathcomp.group_representation.classfun]
cfQuo_char [prf, in mathcomp.group_representation.character]
cfQuo_charE [prf, in mathcomp.group_representation.character]
cfQuo_eq1 [prf, in mathcomp.group_representation.classfun]
cfQuo_irr [prf, in mathcomp.group_representation.character]
cfQuo_iso [prf, in mathcomp.group_representation.classfun]
cfQuo_lin_char [prf, in mathcomp.group_representation.character]
cfQuo_lin_charE [prf, in mathcomp.group_representation.character]
cfQuoE [prf, in mathcomp.group_representation.classfun]
cfQuoEker [prf, in mathcomp.group_representation.classfun]
cfQuoEnorm [prf, in mathcomp.group_representation.classfun]
cfQuoEout [prf, in mathcomp.group_representation.classfun]
cfQuoInorm [prf, in mathcomp.group_representation.classfun]
cfQuoK [prf, in mathcomp.group_representation.classfun]
cfReg_char [prf, in mathcomp.group_representation.character]
cfReg_sum [prf, in mathcomp.group_representation.character]
cfRegE [prf, in mathcomp.group_representation.character]
cfRepr0 [prf, in mathcomp.group_representation.character]
cfRepr1 [prf, in mathcomp.group_representation.character]
cfRepr_char [prf, in mathcomp.group_representation.character]
cfRepr_dadd [prf, in mathcomp.group_representation.character]
cfRepr_dsum [prf, in mathcomp.group_representation.character]
cfRepr_gring_center [prf, in mathcomp.group_representation.integral_char]
cfRepr_inj [prf, in mathcomp.group_representation.character]
cfRepr_map [prf, in mathcomp.group_representation.character]
cfRepr_morphim [prf, in mathcomp.group_representation.character]
cfRepr_muln [prf, in mathcomp.group_representation.character]
cfRepr_prod [prf, in mathcomp.group_representation.character]
cfRepr_rsimP [prf, in mathcomp.group_representation.character]
cfRepr_sim [prf, in mathcomp.group_representation.character]
cfRepr_standard [prf, in mathcomp.group_representation.character]
cfRepr_sub [prf, in mathcomp.group_representation.character]
cfReprReg [prf, in mathcomp.group_representation.character]
cfRes1 [prf, in mathcomp.group_representation.classfun]
cfRes_cfun1 [prf, in mathcomp.group_representation.classfun]
cfRes_char [prf, in mathcomp.group_representation.character]
cfRes_eq0 [prf, in mathcomp.group_representation.character]
cfRes_id [prf, in mathcomp.group_representation.classfun]
cfRes_Ind_invariant [prf, in mathcomp.group_representation.inertia]
cfRes_irr_irr [prf, in mathcomp.group_representation.character]
cfRes_is_linear [prf, in mathcomp.group_representation.classfun]
cfRes_is_monoid_morphism [prf, in mathcomp.group_representation.classfun]
cfRes_lin_char [prf, in mathcomp.group_representation.character]
cfRes_lin_lin [prf, in mathcomp.group_representation.character]
cfRes_prime_irr_cases [prf, in mathcomp.group_representation.inertia]
cfRes_sdprodK [prf, in mathcomp.group_representation.classfun]
cfRes_sub_ker [prf, in mathcomp.group_representation.classfun]
cfRes_vchar [prf, in mathcomp.group_representation.vcharacter]
cfRes_vchar_on [prf, in mathcomp.group_representation.vcharacter]
cfResE [prf, in mathcomp.group_representation.classfun]
cfResEout [prf, in mathcomp.group_representation.classfun]
cfResInd [prf, in mathcomp.group_representation.inertia]
cfResIsom [prf, in mathcomp.group_representation.classfun]
cfResMod [prf, in mathcomp.group_representation.classfun]
cfResMorph [prf, in mathcomp.group_representation.classfun]
cfResQuo [prf, in mathcomp.group_representation.classfun]
cfResRes [prf, in mathcomp.group_representation.classfun]
cfSdprod1 [prf, in mathcomp.group_representation.classfun]
cfSdprod_char [prf, in mathcomp.group_representation.character]
cfSdprod_eq1 [prf, in mathcomp.group_representation.classfun]
cfSdprod_inj [prf, in mathcomp.group_representation.classfun]
cfSdprod_irr [prf, in mathcomp.group_representation.character]
cfSdprod_is_monoid_morphism [prf, in mathcomp.group_representation.classfun]
cfSdprod_is_scalable [prf, in mathcomp.group_representation.classfun]
cfSdprod_is_zmod_morphism [prf, in mathcomp.group_representation.classfun]
cfSdprod_iso [prf, in mathcomp.group_representation.classfun]
cfSdprod_lin_char [prf, in mathcomp.group_representation.character]
cfSdprodE [prf, in mathcomp.group_representation.classfun]
cfSdprodEr [prf, in mathcomp.group_representation.classfun]
cfSdprodK [prf, in mathcomp.group_representation.classfun]
cfSdprodKey [prf, in mathcomp.group_representation.classfun]
cfun0 [prf, in mathcomp.group_representation.classfun]
cfun0_char [prf, in mathcomp.group_representation.character]
cfun0_zchar [prf, in mathcomp.group_representation.vcharacter]
cfun0gen [prf, in mathcomp.group_representation.classfun]
cfun11 [prf, in mathcomp.group_representation.classfun]
cfun1_char [prf, in mathcomp.group_representation.character]
cfun1_irr [prf, in mathcomp.group_representation.character]
cfun1_lin_char [prf, in mathcomp.group_representation.character]
cfun1_vchar [prf, in mathcomp.group_representation.vcharacter]
cfun1E [prf, in mathcomp.group_representation.classfun]
cfun1Egen [prf, in mathcomp.group_representation.classfun]
cfun_add0 [prf, in mathcomp.group_representation.classfun]
cfun_addA [prf, in mathcomp.group_representation.classfun]
cfun_addC [prf, in mathcomp.group_representation.classfun]
cfun_addN [prf, in mathcomp.group_representation.classfun]
cfun_base_free [prf, in mathcomp.group_representation.classfun]
cfun_classE [prf, in mathcomp.group_representation.classfun]
cfun_complement [prf, in mathcomp.group_representation.classfun]
cfun_in_genP [prf, in mathcomp.group_representation.classfun]
cfun_inP [prf, in mathcomp.group_representation.classfun]
cfun_inv0id [prf, in mathcomp.group_representation.classfun]
cfun_irr_sum [prf, in mathcomp.group_representation.character]
cfun_mul1 [prf, in mathcomp.group_representation.classfun]
cfun_mulA [prf, in mathcomp.group_representation.classfun]
cfun_mulC [prf, in mathcomp.group_representation.classfun]
cfun_mulD [prf, in mathcomp.group_representation.classfun]
cfun_mulV [prf, in mathcomp.group_representation.classfun]
cfun_nz1 [prf, in mathcomp.group_representation.classfun]
cfun_on0 [prf, in mathcomp.group_representation.classfun]
cfun_on_sum [prf, in mathcomp.group_representation.classfun]
cfun_onD1 [prf, in mathcomp.group_representation.classfun]
cfun_onE [prf, in mathcomp.group_representation.classfun]
cfun_onG [prf, in mathcomp.group_representation.classfun]
cfun_onP [prf, in mathcomp.group_representation.classfun]
cfun_onS [prf, in mathcomp.group_representation.classfun]
cfun_onT [prf, in mathcomp.group_representation.classfun]
cfun_repr [prf, in mathcomp.group_representation.classfun]
cfun_scale1 [prf, in mathcomp.group_representation.classfun]
cfun_scaleA [prf, in mathcomp.group_representation.classfun]
cfun_scaleAl [prf, in mathcomp.group_representation.classfun]
cfun_scaleDl [prf, in mathcomp.group_representation.classfun]
cfun_scaleDr [prf, in mathcomp.group_representation.classfun]
cfun_sum_cfdot [prf, in mathcomp.group_representation.character]
cfun_sum_constt [prf, in mathcomp.group_representation.character]
cfun_sum_dconstt [prf, in mathcomp.group_representation.vcharacter]
cfun_unitP [prf, in mathcomp.group_representation.classfun]
cfun_vect_iso [prf, in mathcomp.group_representation.classfun]
cfunD1E [prf, in mathcomp.group_representation.classfun]
cfunE [prf, in mathcomp.group_representation.classfun]
cfunElock [prf, in mathcomp.group_representation.classfun]
cfunGid [prf, in mathcomp.group_representation.classfun]
cfuni_on [prf, in mathcomp.group_representation.classfun]
cfuniE [prf, in mathcomp.group_representation.classfun]
cfuniG [prf, in mathcomp.group_representation.classfun]
cfunJ [prf, in mathcomp.group_representation.classfun]
cfunJgen [prf, in mathcomp.group_representation.classfun]
cfunM_on [prf, in mathcomp.group_representation.classfun]
cfunM_onI [prf, in mathcomp.group_representation.classfun]
cfunP [prf, in mathcomp.group_representation.classfun]
char1 [prf, in mathcomp.finite_group.automorphism]
char1_eq0 [prf, in mathcomp.group_representation.character]
char1_ge0 [prf, in mathcomp.group_representation.character]
char1_ge_constt [prf, in mathcomp.group_representation.character]
char1_ge_norm [prf, in mathcomp.group_representation.character]
char1_gt0 [prf, in mathcomp.group_representation.character]
char_abelianP [prf, in mathcomp.group_representation.character]
char_block_diag_mx [prf, in mathcomp.algebra.mxpoly]
char_cfcenterE [prf, in mathcomp.group_representation.character]
char_from_quotient [prf, in mathcomp.finite_group.quotient]
char_injm [prf, in mathcomp.finite_group.automorphism]
char_inv [prf, in mathcomp.group_representation.character]
char_nmod_closed [prf, in mathcomp.group_representation.character]
char_norm [prf, in mathcomp.finite_group.automorphism]
char_norm_trans [prf, in mathcomp.finite_group.automorphism]
char_normal [prf, in mathcomp.finite_group.automorphism]
char_normal_trans [prf, in mathcomp.finite_group.automorphism]
char_norms [prf, in mathcomp.finite_group.automorphism]
char_poly_det [prf, in mathcomp.algebra.mxpoly]
char_poly_monic [prf, in mathcomp.algebra.mxpoly]
char_poly_trace [prf, in mathcomp.algebra.mxpoly]
char_poly_trig [prf, in mathcomp.algebra.mxpoly]
char_refl [prf, in mathcomp.finite_group.automorphism]
char_reprP [prf, in mathcomp.group_representation.character]
char_sub [prf, in mathcomp.finite_group.automorphism]
char_sum_irr [prf, in mathcomp.group_representation.character]
char_sum_irrP [prf, in mathcomp.group_representation.character]
char_trans [prf, in mathcomp.finite_group.automorphism]
char_vchar [prf, in mathcomp.group_representation.vcharacter]
character_table_unit [prf, in mathcomp.group_representation.character]
charI [prf, in mathcomp.finite_group.automorphism]
charM [prf, in mathcomp.finite_group.automorphism]
charP [prf, in mathcomp.finite_group.automorphism]
charR [prf, in mathcomp.solvable.commutator]
charsimple_dprod [prf, in mathcomp.solvable.maximal]
charsimple_solvable [prf, in mathcomp.solvable.maximal]
charsimpleP [prf, in mathcomp.solvable.maximal]
charY [prf, in mathcomp.finite_group.automorphism]
chief_factor_minnormal [prf, in mathcomp.solvable.gseries]
chief_series_exists [prf, in mathcomp.solvable.gseries]
chinese_mod [prf, in mathcomp.boot.div]
chinese_modl [prf, in mathcomp.boot.div]
chinese_modr [prf, in mathcomp.boot.div]
chinese_remainder [prf, in mathcomp.boot.div]
choose_id [prf, in mathcomp.boot.choice]
chooseP [prf, in mathcomp.boot.choice]
Cint_cfdot_vchar [prf, in mathcomp.group_representation.vcharacter]
Cint_cfdot_vchar_irr [prf, in mathcomp.group_representation.vcharacter]
Cint_rat [prf, in mathcomp.field.algC]
Cint_rat_Aint [prf, in mathcomp.field.algnum]
Cint_span_zmod_closed [prf, in mathcomp.field.algnum]
Cint_spanP [prf, in mathcomp.field.algnum]
Cint_vchar1 [prf, in mathcomp.group_representation.vcharacter]
Cintr_Cyclotomic [prf, in mathcomp.field.cyclotomic]
class1G [prf, in mathcomp.finite_group.fingroup]
class1g [prf, in mathcomp.finite_group.fingroup]
class_eqP [prf, in mathcomp.finite_group.fingroup]
class_formula [prf, in mathcomp.finite_group.action]
class_IirrK [prf, in mathcomp.group_representation.character]
class_lcoset [prf, in mathcomp.finite_group.fingroup]
class_norm [prf, in mathcomp.finite_group.fingroup]
class_normal [prf, in mathcomp.finite_group.fingroup]
class_rcoset [prf, in mathcomp.finite_group.fingroup]
class_refl [prf, in mathcomp.finite_group.fingroup]
class_set1 [prf, in mathcomp.finite_group.fingroup]
class_sub_norm [prf, in mathcomp.finite_group.fingroup]
class_subG [prf, in mathcomp.finite_group.fingroup]
class_support_id [prf, in mathcomp.finite_group.fingroup]
class_support_norm [prf, in mathcomp.finite_group.fingroup]
class_support_set1l [prf, in mathcomp.finite_group.fingroup]
class_support_set1r [prf, in mathcomp.finite_group.fingroup]
class_support_sub_norm [prf, in mathcomp.finite_group.fingroup]
class_support_subG [prf, in mathcomp.finite_group.fingroup]
class_supportD1 [prf, in mathcomp.finite_group.fingroup]
class_supportEl [prf, in mathcomp.finite_group.fingroup]
class_supportEr [prf, in mathcomp.finite_group.fingroup]
class_supportGidl [prf, in mathcomp.finite_group.fingroup]
class_supportGidr [prf, in mathcomp.finite_group.fingroup]
class_supportM [prf, in mathcomp.finite_group.fingroup]
class_sym [prf, in mathcomp.finite_group.fingroup]
class_trans [prf, in mathcomp.finite_group.fingroup]
class_transl [prf, in mathcomp.finite_group.fingroup]
classes1 [prf, in mathcomp.finite_group.fingroup]
classes_gt0 [prf, in mathcomp.finite_group.fingroup]
classes_gt1 [prf, in mathcomp.finite_group.fingroup]
classes_morphim [prf, in mathcomp.finite_group.morphism]
classes_partition [prf, in mathcomp.finite_group.action]
classes_quotient [prf, in mathcomp.finite_group.quotient]
classfun_key [prf, in mathcomp.group_representation.classfun]
classg_base_center [prf, in mathcomp.group_representation.mxrepresentation]
classg_base_free [prf, in mathcomp.group_representation.mxrepresentation]
classG_eq1 [prf, in mathcomp.finite_group.fingroup]
classGidl [prf, in mathcomp.finite_group.fingroup]
classGidr [prf, in mathcomp.finite_group.fingroup]
classM [prf, in mathcomp.finite_group.fingroup]
classS [prf, in mathcomp.finite_group.fingroup]
classVg [prf, in mathcomp.finite_group.fingroup]
Clifford_astab [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_astab1 [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_atrans [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_basis [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_component_basis [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_componentJ [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_hom [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_is_action [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_iso [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_iso2 [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_rank_components [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_Res_sum_cfclass [prf, in mathcomp.group_representation.inertia]
Clifford_rstabs_simple [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_simple [prf, in mathcomp.group_representation.mxrepresentation]
Clifford_Socle1 [prf, in mathcomp.group_representation.mxrepresentation]
closed_connect [prf, in mathcomp.boot.fingraph]
closed_field_poly_normal [prf, in mathcomp.algebra.poly]
closed_nonrootP [prf, in mathcomp.algebra.poly]
closed_rootP [prf, in mathcomp.algebra.poly]
ClosedFieldQE.abstrX1 [prf, in mathcomp.field.closed_field]
ClosedFieldQE.abstrX_mulM [prf, in mathcomp.field.closed_field]
ClosedFieldQE.abstrXP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_amulXnT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_lift [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_mulpT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_natmulpT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_opppT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_poly1 [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_poly_mulM [prf, in mathcomp.field.closed_field]
ClosedFieldQE.eval_sumpT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.ex_elim_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.ex_elim_seq_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.ex_elim_seqP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.holds_conj [prf, in mathcomp.field.closed_field]
ClosedFieldQE.holds_conjn [prf, in mathcomp.field.closed_field]
ClosedFieldQE.holds_ex_elim [prf, in mathcomp.field.closed_field]
ClosedFieldQE.isnull_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.isnullP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.lead_coefT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.lead_coefTP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.qf_cps_bind [prf, in mathcomp.field.closed_field]
ClosedFieldQE.qf_cps_if [prf, in mathcomp.field.closed_field]
ClosedFieldQE.qf_cps_ret [prf, in mathcomp.field.closed_field]
ClosedFieldQE.qf_simpl [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rabstrX [prf, in mathcomp.field.closed_field]
ClosedFieldQE.ramulXnT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.redivp_rec_loopP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.redivp_rec_loopT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.redivp_rec_loopTP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.redivpT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.redivpTP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgcdp_loopP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgcdp_loopT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgcdpT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgcdpTP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgcdpTs_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgcdpTsP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgdcop_recT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgdcop_recTP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgdcopT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rgdcopTP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rmulpT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rpoly_map_mul [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rseq_poly_map [prf, in mathcomp.field.closed_field]
ClosedFieldQE.rsumpT [prf, in mathcomp.field.closed_field]
ClosedFieldQE.sizeT_qf [prf, in mathcomp.field.closed_field]
ClosedFieldQE.sizeTP [prf, in mathcomp.field.closed_field]
ClosedFieldQE.wf_ex_elim [prf, in mathcomp.field.closed_field]
closure_closed [prf, in mathcomp.boot.fingraph]
cmp0 [prf, in mathcomp.algebra.interval_inference]
Cnat_cfdot_char [prf, in mathcomp.group_representation.character]
Cnat_cfdot_char_irr [prf, in mathcomp.group_representation.character]
Cnat_cfnorm_vchar [prf, in mathcomp.group_representation.vcharacter]
Cnat_char1 [prf, in mathcomp.group_representation.character]
Cnat_dirr [prf, in mathcomp.group_representation.vcharacter]
Cnat_irr1 [prf, in mathcomp.group_representation.character]
cnorm_dconstt [prf, in mathcomp.group_representation.vcharacter]
CodeSeq.codeK [prf, in mathcomp.boot.choice]
CodeSeq.decodeK [prf, in mathcomp.boot.choice]
CodeSeq.gtn_decode [prf, in mathcomp.boot.choice]
CodeSeq.ltn_code [prf, in mathcomp.boot.choice]
codiagonalizable1 [prf, in mathcomp.algebra.mxred]
codiagonalizable1 [prf, in mathcomp.algebra.mxpoly]
codiagonalizable_on [prf, in mathcomp.algebra.mxred]
codiagonalizable_on [prf, in mathcomp.algebra.mxpoly]
codiagonalizableP [prf, in mathcomp.algebra.mxred]
codiagonalizableP [prf, in mathcomp.algebra.mxpoly]
codiagonalizablePfull [prf, in mathcomp.algebra.mxred]
codom_f [prf, in mathcomp.boot.fintype]
codom_ffun [prf, in mathcomp.boot.finfun]
codom_tffun [prf, in mathcomp.boot.finfun]
codom_val [prf, in mathcomp.boot.fintype]
codomE [prf, in mathcomp.boot.fintype]
codomP [prf, in mathcomp.boot.fintype]
coef0 [prf, in mathcomp.algebra.poly]
coef0_prod [prf, in mathcomp.algebra.poly]
coef0_prod_XsubC [prf, in mathcomp.algebra.poly]
coef0M [prf, in mathcomp.algebra.poly]
coef1 [prf, in mathcomp.algebra.poly]
coef_add_poly [prf, in mathcomp.algebra.poly]
coef_comp_poly [prf, in mathcomp.algebra.poly]
coef_comp_poly_Xn [prf, in mathcomp.algebra.poly]
coef_cons [prf, in mathcomp.algebra.poly]
coef_deriv [prf, in mathcomp.algebra.poly]
coef_derivn [prf, in mathcomp.algebra.poly]
coef_drop_poly [prf, in mathcomp.algebra.poly]
coef_even_poly [prf, in mathcomp.algebra.poly]
coef_map [prf, in mathcomp.algebra.poly]
coef_map_id0 [prf, in mathcomp.algebra.poly]
coef_mul_poly [prf, in mathcomp.algebra.poly]
coef_mul_poly_rev [prf, in mathcomp.algebra.poly]
coef_nderivn [prf, in mathcomp.algebra.poly]
coef_npolyp [prf, in mathcomp.algebra.qpoly]
coef_odd_poly [prf, in mathcomp.algebra.poly]
coef_opp_poly [prf, in mathcomp.algebra.poly]
coef_poly [prf, in mathcomp.algebra.poly]
coef_Poly [prf, in mathcomp.algebra.poly]
coef_prod_XsubC [prf, in mathcomp.algebra.poly]
coef_rVpoly [prf, in mathcomp.algebra.mxpoly]
coef_rVpoly_ord [prf, in mathcomp.algebra.mxpoly]
coef_sum [prf, in mathcomp.algebra.poly]
coef_sumMXn [prf, in mathcomp.algebra.poly]
coef_swapXY [prf, in mathcomp.algebra.polyXY]
coef_take_poly [prf, in mathcomp.algebra.poly]
coefB [prf, in mathcomp.algebra.poly]
coefC [prf, in mathcomp.algebra.poly]
coefCM [prf, in mathcomp.algebra.poly]
coefD [prf, in mathcomp.algebra.poly]
coefK [prf, in mathcomp.algebra.poly]
coefM [prf, in mathcomp.algebra.poly]
coefMC [prf, in mathcomp.algebra.poly]
coefMn [prf, in mathcomp.algebra.poly]
coefMNn [prf, in mathcomp.algebra.poly]
coefMr [prf, in mathcomp.algebra.poly]
coefMrz [prf, in mathcomp.algebra.ssrint]
coefMX [prf, in mathcomp.algebra.poly]
coefMXn [prf, in mathcomp.algebra.poly]
coefN [prf, in mathcomp.algebra.poly]
coefn_sum [prf, in mathcomp.algebra.qpoly]
coefp0_is_monoid_morphism [prf, in mathcomp.algebra.poly]
coefPn_prod_XsubC [prf, in mathcomp.algebra.poly]
coefX [prf, in mathcomp.algebra.poly]
coefXM [prf, in mathcomp.algebra.poly]
coefXn [prf, in mathcomp.algebra.poly]
coefXnM [prf, in mathcomp.algebra.poly]
coefZ [prf, in mathcomp.algebra.poly]
cofactor_map_mx [prf, in mathcomp.algebra.matrix]
cofactor_tr [prf, in mathcomp.algebra.matrix]
cofactorZ [prf, in mathcomp.algebra.matrix]
cofixsetK [prf, in mathcomp.boot.finset]
cokermx_eq0 [prf, in mathcomp.algebra.mxalgebra]
col'_col_mx [prf, in mathcomp.algebra.matrix]
col'_const [prf, in mathcomp.algebra.matrix]
col'_eq [prf, in mathcomp.algebra.matrix]
col'Esub [prf, in mathcomp.algebra.matrix]
col'Kl [prf, in mathcomp.algebra.matrix]
col'Kr [prf, in mathcomp.algebra.matrix]
col0 [prf, in mathcomp.algebra.matrix]
col1 [prf, in mathcomp.algebra.matrix]
col_base_full [prf, in mathcomp.algebra.mxalgebra]
col_col_mx [prf, in mathcomp.algebra.matrix]
col_colsub [prf, in mathcomp.algebra.matrix]
col_const [prf, in mathcomp.algebra.matrix]
col_ebase_unit [prf, in mathcomp.algebra.mxalgebra]
col_eq [prf, in mathcomp.algebra.matrix]
col_flat_mx [prf, in mathcomp.algebra.matrix]
col_id [prf, in mathcomp.algebra.matrix]
col_ind [prf, in mathcomp.algebra.matrix]
col_leq_rank [prf, in mathcomp.algebra.mxalgebra]
col_lsubmx [prf, in mathcomp.algebra.matrix]
col_mx0 [prf, in mathcomp.algebra.matrix]
col_mx_const [prf, in mathcomp.algebra.matrix]
col_mx_eq0 [prf, in mathcomp.algebra.matrix]
col_mx_key [prf, in mathcomp.algebra.matrix]
col_mx_sub [prf, in mathcomp.algebra.mxalgebra]
col_mxA [prf, in mathcomp.algebra.matrix]
col_mxblock [prf, in mathcomp.algebra.matrix]
col_mxcol [prf, in mathcomp.algebra.matrix]
col_mxdiag [prf, in mathcomp.algebra.matrix]
col_mxEd [prf, in mathcomp.algebra.matrix]
col_mxEu [prf, in mathcomp.algebra.matrix]
col_mxKd [prf, in mathcomp.algebra.matrix]
col_mxKu [prf, in mathcomp.algebra.matrix]
col_mxrow [prf, in mathcomp.algebra.matrix]
col_mxsub [prf, in mathcomp.algebra.matrix]
col_perm1 [prf, in mathcomp.algebra.matrix]
col_perm_const [prf, in mathcomp.algebra.matrix]
col_perm_key [prf, in mathcomp.algebra.matrix]
col_permE [prf, in mathcomp.algebra.matrix]
col_permEsub [prf, in mathcomp.algebra.matrix]
col_permM [prf, in mathcomp.algebra.matrix]
col_row_permC [prf, in mathcomp.algebra.matrix]
col_rsubmx [prf, in mathcomp.algebra.matrix]
colE [prf, in mathcomp.algebra.matrix]
colEsub [prf, in mathcomp.algebra.matrix]
colKl [prf, in mathcomp.algebra.matrix]
colKr [prf, in mathcomp.algebra.matrix]
colP [prf, in mathcomp.algebra.matrix]
colsub_cast [prf, in mathcomp.algebra.matrix]
colsub_comp [prf, in mathcomp.algebra.matrix]
comm0mx [prf, in mathcomp.algebra.matrix]
comm1G [prf, in mathcomp.solvable.commutator]
comm1g [prf, in mathcomp.boot.monoid]
comm1mx [prf, in mathcomp.algebra.matrix]
comm3G1P [prf, in mathcomp.solvable.commutator]
comm_coef_poly [prf, in mathcomp.algebra.poly]
comm_group_setP [prf, in mathcomp.finite_group.fingroup]
comm_horner_mx [prf, in mathcomp.algebra.mxpoly]
comm_horner_mx2 [prf, in mathcomp.algebra.mxpoly]
comm_joingE [prf, in mathcomp.finite_group.fingroup]
comm_mx0 [prf, in mathcomp.algebra.matrix]
comm_mx1 [prf, in mathcomp.algebra.matrix]
comm_mx_horner [prf, in mathcomp.algebra.mxpoly]
comm_mx_refl [prf, in mathcomp.algebra.matrix]
comm_mx_scalar [prf, in mathcomp.algebra.matrix]
comm_mx_stable [prf, in mathcomp.algebra.mxalgebra]
comm_mx_stable_eigenspace [prf, in mathcomp.algebra.mxalgebra]
comm_mx_stable_geigenspace [prf, in mathcomp.algebra.mxpoly]
comm_mx_stable_ker [prf, in mathcomp.algebra.mxalgebra]
comm_mx_stable_kermxpoly [prf, in mathcomp.algebra.mxpoly]
comm_mx_sum [prf, in mathcomp.algebra.matrix]
comm_mx_sym [prf, in mathcomp.algebra.matrix]
comm_mxB [prf, in mathcomp.algebra.matrix]
comm_mxD [prf, in mathcomp.algebra.matrix]
comm_mxE [prf, in mathcomp.algebra.matrix]
comm_mxM [prf, in mathcomp.algebra.matrix]
comm_mxN [prf, in mathcomp.algebra.matrix]
comm_mxN1 [prf, in mathcomp.algebra.matrix]
comm_mxP [prf, in mathcomp.algebra.matrix]
comm_norm_cent_cent [prf, in mathcomp.solvable.commutator]
comm_poly0 [prf, in mathcomp.algebra.poly]
comm_poly1 [prf, in mathcomp.algebra.poly]
comm_poly_exp [prf, in mathcomp.algebra.poly]
comm_polyD [prf, in mathcomp.algebra.poly]
comm_polyM [prf, in mathcomp.algebra.poly]
comm_polyX [prf, in mathcomp.algebra.poly]
comm_prodG [prf, in mathcomp.finite_group.gproduct]
comm_scalar_mx [prf, in mathcomp.algebra.matrix]
comm_sub_max_pgroup [prf, in mathcomp.solvable.pgroup]
comm_subG [prf, in mathcomp.finite_group.fingroup]
commG1 [prf, in mathcomp.solvable.commutator]
commg1 [prf, in mathcomp.boot.monoid]
commg1_sym [prf, in mathcomp.boot.monoid]
commG1P [prf, in mathcomp.finite_group.fingroup]
commg_norm [prf, in mathcomp.solvable.commutator]
commg_normal [prf, in mathcomp.solvable.commutator]
commg_norml [prf, in mathcomp.solvable.commutator]
commg_normr [prf, in mathcomp.solvable.commutator]
commg_normSl [prf, in mathcomp.solvable.commutator]
commg_normSr [prf, in mathcomp.solvable.commutator]
commg_sub [prf, in mathcomp.solvable.commutator]
commg_subI [prf, in mathcomp.solvable.commutator]
commg_subl [prf, in mathcomp.solvable.commutator]
commg_subr [prf, in mathcomp.solvable.commutator]
commgAC [prf, in mathcomp.solvable.commutator]
commGC [prf, in mathcomp.finite_group.fingroup]
commgC [prf, in mathcomp.boot.monoid]
commgCV [prf, in mathcomp.boot.monoid]
commgEl [prf, in mathcomp.boot.monoid]
commgEr [prf, in mathcomp.boot.monoid]
commgg [prf, in mathcomp.boot.monoid]
commgMJ [prf, in mathcomp.solvable.commutator]
commgMR [prf, in mathcomp.solvable.commutator]
commgP [prf, in mathcomp.boot.monoid]
commgS [prf, in mathcomp.finite_group.fingroup]
commgSS [prf, in mathcomp.finite_group.fingroup]
commgV [prf, in mathcomp.solvable.commutator]
commgVg [prf, in mathcomp.boot.monoid]
commgX [prf, in mathcomp.solvable.commutator]
commgXg [prf, in mathcomp.boot.monoid]
commgXVg [prf, in mathcomp.boot.monoid]
commMG [prf, in mathcomp.solvable.commutator]
commMgJ [prf, in mathcomp.solvable.commutator]
commMGr [prf, in mathcomp.solvable.commutator]
commMgR [prf, in mathcomp.solvable.commutator]
common_eigenvector [prf, in mathcomp.algebra.spectral]
common_eigenvector2 [prf, in mathcomp.algebra.spectral]
commr_horner [prf, in mathcomp.algebra.poly]
commr_int [prf, in mathcomp.algebra.ssrint]
commr_polyX [prf, in mathcomp.algebra.poly]
commr_polyXn [prf, in mathcomp.algebra.poly]
commrMz [prf, in mathcomp.algebra.ssrint]
commrXz [prf, in mathcomp.algebra.ssrint]
commrXz_wmulls [prf, in mathcomp.algebra.ssrint]
commSg [prf, in mathcomp.finite_group.fingroup]
commute1 [prf, in mathcomp.boot.monoid]
commute_prod [prf, in mathcomp.boot.monoid]
commute_refl [prf, in mathcomp.boot.monoid]
commute_sym [prf, in mathcomp.boot.monoid]
commuteM [prf, in mathcomp.boot.monoid]
commuteV [prf, in mathcomp.boot.monoid]
commuteX [prf, in mathcomp.boot.monoid]
commuteX2 [prf, in mathcomp.boot.monoid]
commVg [prf, in mathcomp.solvable.commutator]
commXg [prf, in mathcomp.solvable.commutator]
commXXg [prf, in mathcomp.solvable.commutator]
comp_actE [prf, in mathcomp.finite_group.action]
comp_gmulf1 [prf, in mathcomp.boot.monoid]
comp_gmulfM [prf, in mathcomp.boot.monoid]
comp_is_action [prf, in mathcomp.finite_group.action]
comp_is_ahom [prf, in mathcomp.field.falgebra]
comp_is_groupAction [prf, in mathcomp.finite_group.action]
comp_kHom [prf, in mathcomp.field.galois]
comp_kHom_img [prf, in mathcomp.field.galois]
comp_lfun0l [prf, in mathcomp.algebra.vector]
comp_lfun0r [prf, in mathcomp.algebra.vector]
comp_lfun1l [prf, in mathcomp.algebra.vector]
comp_lfun1r [prf, in mathcomp.algebra.vector]
comp_lfunA [prf, in mathcomp.algebra.vector]
comp_lfunDl [prf, in mathcomp.algebra.vector]
comp_lfunDr [prf, in mathcomp.algebra.vector]
comp_lfunE [prf, in mathcomp.algebra.vector]
comp_lfunNl [prf, in mathcomp.algebra.vector]
comp_lfunNr [prf, in mathcomp.algebra.vector]
comp_lfunZl [prf, in mathcomp.algebra.vector]
comp_lfunZr [prf, in mathcomp.algebra.vector]
comp_morphM [prf, in mathcomp.finite_group.morphism]
comp_poly0 [prf, in mathcomp.algebra.poly]
comp_poly0r [prf, in mathcomp.algebra.poly]
comp_poly2_eq0 [prf, in mathcomp.algebra.poly]
comp_poly_eq0 [prf, in mathcomp.algebra.poly]
comp_poly_is_linear [prf, in mathcomp.algebra.poly]
comp_poly_is_monoid_morphism [prf, in mathcomp.algebra.poly]
comp_poly_is_semilinear [prf, in mathcomp.algebra.poly]
comp_poly_MXaddC [prf, in mathcomp.algebra.poly]
comp_poly_Xn [prf, in mathcomp.algebra.poly]
comp_polyA [prf, in mathcomp.algebra.poly]
comp_polyB [prf, in mathcomp.algebra.poly]
comp_polyC [prf, in mathcomp.algebra.poly]
comp_polyCr [prf, in mathcomp.algebra.poly]
comp_polyD [prf, in mathcomp.algebra.poly]
comp_polyE [prf, in mathcomp.algebra.poly]
comp_polyM [prf, in mathcomp.algebra.poly]
comp_polyX [prf, in mathcomp.algebra.poly]
comp_polyXaddC_K [prf, in mathcomp.algebra.poly]
comp_polyXr [prf, in mathcomp.algebra.poly]
comp_polyZ [prf, in mathcomp.algebra.poly]
comp_reprGLm [prf, in mathcomp.group_representation.mxabelem]
comp_Xn_poly [prf, in mathcomp.algebra.poly]
companion_map_poly [prf, in mathcomp.algebra.mxpoly]
companionmxK [prf, in mathcomp.algebra.mxpoly]
comparable_BSide_max [prf, in mathcomp.algebra.interval]
comparable_BSide_min [prf, in mathcomp.algebra.interval]
compareP [prf, in mathcomp.boot.eqtype]
compl_p'Hall [prf, in mathcomp.solvable.pgroup]
compl_pHall [prf, in mathcomp.solvable.pgroup]
complete_unitmx [prf, in mathcomp.algebra.mxalgebra]
complgC [prf, in mathcomp.finite_group.gproduct]
complP [prf, in mathcomp.finite_group.gproduct]
component_mx_def [prf, in mathcomp.group_representation.mxrepresentation]
component_mx_disjoint [prf, in mathcomp.group_representation.mxrepresentation]
component_mx_id [prf, in mathcomp.group_representation.mxrepresentation]
component_mx_iso [prf, in mathcomp.group_representation.mxrepresentation]
component_mx_isoP [prf, in mathcomp.group_representation.mxrepresentation]
component_mx_key [prf, in mathcomp.group_representation.mxrepresentation]
component_mx_module [prf, in mathcomp.group_representation.mxrepresentation]
component_mx_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
component_socle [prf, in mathcomp.group_representation.mxrepresentation]
comps_cons [prf, in mathcomp.solvable.jordanholder]
compsP [prf, in mathcomp.solvable.jordanholder]
conform_castmx [prf, in mathcomp.algebra.matrix]
conform_mx_id [prf, in mathcomp.algebra.matrix]
congr_big [prf, in mathcomp.boot.bigop]
congr_big_nat [prf, in mathcomp.boot.bigop]
congr_group [prf, in mathcomp.finite_group.fingroup]
congr_irr [prf, in mathcomp.group_representation.character]
congr_subg [prf, in mathcomp.finite_group.fingroup]
congr_subvs [prf, in mathcomp.algebra.vector]
conj0g [prf, in mathcomp.finite_group.fingroup]
conj0mx [prf, in mathcomp.algebra.mxred]
conj0mx [prf, in mathcomp.algebra.mxpoly]
conj1g [prf, in mathcomp.boot.monoid]
conj1mx [prf, in mathcomp.algebra.mxred]
conj1mx [prf, in mathcomp.algebra.mxpoly]
conj_astabQ [prf, in mathcomp.finite_group.action]
conj_aut_morphM [prf, in mathcomp.finite_group.automorphism]
conj_autE [prf, in mathcomp.finite_group.automorphism]
conj_cfConjg [prf, in mathcomp.group_representation.inertia]
conj_Crat [prf, in mathcomp.field.algC]
conj_isog [prf, in mathcomp.finite_group.automorphism]
conj_isom [prf, in mathcomp.finite_group.automorphism]
conj_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
conj_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
conj_subG [prf, in mathcomp.finite_group.fingroup]
conjC_charAut [prf, in mathcomp.group_representation.character]
conjC_Iirr0 [prf, in mathcomp.group_representation.character]
conjC_Iirr_eq0 [prf, in mathcomp.group_representation.character]
conjC_IirrE [prf, in mathcomp.group_representation.character]
conjC_IirrK [prf, in mathcomp.group_representation.character]
conjC_irrAut [prf, in mathcomp.group_representation.character]
conjC_pair_orthogonal [prf, in mathcomp.group_representation.classfun]
conjC_unitary [prf, in mathcomp.algebra.spectral]
conjC_vcharAut [prf, in mathcomp.group_representation.vcharacter]
conjCg [prf, in mathcomp.finite_group.fingroup]
conjD1g [prf, in mathcomp.finite_group.fingroup]
conjDg [prf, in mathcomp.finite_group.fingroup]
conjg1 [prf, in mathcomp.boot.monoid]
conjg_eq1 [prf, in mathcomp.boot.monoid]
conjg_fix [prf, in mathcomp.boot.monoid]
conjg_fixP [prf, in mathcomp.boot.monoid]
conjg_Iirr0 [prf, in mathcomp.group_representation.inertia]
conjg_Iirr_eq0 [prf, in mathcomp.group_representation.inertia]
conjg_Iirr_inj [prf, in mathcomp.group_representation.inertia]
conjg_IirrE [prf, in mathcomp.group_representation.inertia]
conjg_IirrK [prf, in mathcomp.group_representation.inertia]
conjg_IirrKV [prf, in mathcomp.group_representation.inertia]
conjg_inertia [prf, in mathcomp.group_representation.inertia]
conjg_inj [prf, in mathcomp.boot.monoid]
conjG_is_action [prf, in mathcomp.finite_group.action]
conjg_is_groupAction [prf, in mathcomp.finite_group.action]
conjg_mulR [prf, in mathcomp.solvable.commutator]
conjg_preim [prf, in mathcomp.finite_group.fingroup]
conjg_prod [prf, in mathcomp.boot.monoid]
conjg_Rmul [prf, in mathcomp.solvable.commutator]
conjg_set1 [prf, in mathcomp.finite_group.fingroup]
conjgC [prf, in mathcomp.boot.monoid]
conjgCV [prf, in mathcomp.boot.monoid]
conjgE [prf, in mathcomp.boot.monoid]
conjGid [prf, in mathcomp.finite_group.fingroup]
conjgK [prf, in mathcomp.boot.monoid]
conjgKV [prf, in mathcomp.boot.monoid]
conjgM [prf, in mathcomp.boot.monoid]
conjgmE [prf, in mathcomp.finite_group.automorphism]
conjIg [prf, in mathcomp.finite_group.fingroup]
conjJg [prf, in mathcomp.boot.monoid]
conjMg [prf, in mathcomp.boot.monoid]
conjMmx [prf, in mathcomp.algebra.mxred]
conjMmx [prf, in mathcomp.algebra.mxpoly]
conjMumx [prf, in mathcomp.algebra.mxred]
conjMumx [prf, in mathcomp.algebra.mxpoly]
conjmx0 [prf, in mathcomp.algebra.mxred]
conjmx0 [prf, in mathcomp.algebra.mxpoly]
conjmx_eigenvalue [prf, in mathcomp.algebra.mxred]
conjmx_eigenvalue [prf, in mathcomp.algebra.mxpoly]
conjmx_scalar [prf, in mathcomp.algebra.mxred]
conjmx_scalar [prf, in mathcomp.algebra.mxpoly]
conjmxK [prf, in mathcomp.algebra.mxred]
conjmxK [prf, in mathcomp.algebra.mxpoly]
conjmxM [prf, in mathcomp.algebra.mxred]
conjmxM [prf, in mathcomp.algebra.mxpoly]
conjmxVK [prf, in mathcomp.algebra.mxred]
conjmxVK [prf, in mathcomp.algebra.mxpoly]
conjRg [prf, in mathcomp.boot.monoid]
conjs1g [prf, in mathcomp.finite_group.fingroup]
conjSg [prf, in mathcomp.finite_group.fingroup]
conjsg1 [prf, in mathcomp.finite_group.fingroup]
conjsg_eq1 [prf, in mathcomp.finite_group.fingroup]
conjsg_inj [prf, in mathcomp.finite_group.fingroup]
conjsgE [prf, in mathcomp.finite_group.fingroup]
conjsgK [prf, in mathcomp.finite_group.fingroup]
conjsgKV [prf, in mathcomp.finite_group.fingroup]
conjsgM [prf, in mathcomp.finite_group.fingroup]
conjsMg [prf, in mathcomp.finite_group.fingroup]
conjsRg [prf, in mathcomp.finite_group.fingroup]
conjTg [prf, in mathcomp.finite_group.fingroup]
conjUg [prf, in mathcomp.finite_group.fingroup]
conjugates_conj [prf, in mathcomp.finite_group.fingroup]
conjugates_set1 [prf, in mathcomp.finite_group.fingroup]
conjugatesS [prf, in mathcomp.finite_group.fingroup]
conjuMmx [prf, in mathcomp.algebra.mxred]
conjuMmx [prf, in mathcomp.algebra.mxpoly]
conjuMumx [prf, in mathcomp.algebra.mxred]
conjuMumx [prf, in mathcomp.algebra.mxpoly]
conjumx [prf, in mathcomp.algebra.mxred]
conjumx [prf, in mathcomp.algebra.mxpoly]
conjVg [prf, in mathcomp.boot.monoid]
conjVmx [prf, in mathcomp.algebra.mxred]
conjVmx [prf, in mathcomp.algebra.mxpoly]
conjXg [prf, in mathcomp.boot.monoid]
conjYg [prf, in mathcomp.finite_group.fingroup]
conjymx [prf, in mathcomp.algebra.spectral]
connect0 [prf, in mathcomp.boot.fingraph]
connect1 [prf, in mathcomp.boot.fingraph]
connect_closed [prf, in mathcomp.boot.fingraph]
connect_cycle [prf, in mathcomp.boot.fingraph]
connect_rev [prf, in mathcomp.boot.fingraph]
connect_root [prf, in mathcomp.boot.fingraph]
connect_sub [prf, in mathcomp.boot.fingraph]
connect_trans [prf, in mathcomp.boot.fingraph]
connectP [prf, in mathcomp.boot.fingraph]
cons2_infix [prf, in mathcomp.boot.seq]
cons_poly_def [prf, in mathcomp.algebra.poly]
cons_subseq [prf, in mathcomp.boot.seq]
cons_uniq [prf, in mathcomp.boot.seq]
consl_infix [prf, in mathcomp.boot.seq]
consr_infix [prf, in mathcomp.boot.seq]
const_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
const_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
const_mx_key [prf, in mathcomp.algebra.matrix]
const_t_is_monoid_morphism [prf, in mathcomp.algebra.tensor]
const_t_is_nmod_morphism [prf, in mathcomp.algebra.tensor]
const_tK [prf, in mathcomp.algebra.tensor]
const_tV [prf, in mathcomp.algebra.tensor]
constant_nseq [prf, in mathcomp.boot.seq]
constantP [prf, in mathcomp.boot.seq]
constt0_Res_cfker [prf, in mathcomp.group_representation.inertia]
constt1 [prf, in mathcomp.solvable.pgroup]
constt1P [prf, in mathcomp.solvable.pgroup]
constt_cfInd_irr [prf, in mathcomp.group_representation.character]
constt_cfRes_irr [prf, in mathcomp.group_representation.character]
constt_charP [prf, in mathcomp.group_representation.character]
constt_Ind_ext [prf, in mathcomp.group_representation.inertia]
constt_Ind_mul_ext [prf, in mathcomp.group_representation.inertia]
constt_Ind_Res [prf, in mathcomp.group_representation.character]
constt_Inertia_bijection [prf, in mathcomp.group_representation.inertia]
constt_irr [prf, in mathcomp.group_representation.character]
constt_ortho_char [prf, in mathcomp.group_representation.character]
constt_p_elt [prf, in mathcomp.solvable.pgroup]
constt_Res_trans [prf, in mathcomp.group_representation.character]
consttC [prf, in mathcomp.solvable.pgroup]
consttJ [prf, in mathcomp.solvable.pgroup]
consttM [prf, in mathcomp.solvable.pgroup]
consttNK [prf, in mathcomp.solvable.pgroup]
consttV [prf, in mathcomp.solvable.pgroup]
consttX [prf, in mathcomp.solvable.pgroup]
contra_eq [prf, in mathcomp.boot.eqtype]
contra_eq_neq [prf, in mathcomp.boot.eqtype]
contra_eq_not [prf, in mathcomp.boot.eqtype]
contra_eqF [prf, in mathcomp.boot.eqtype]
contra_eqN [prf, in mathcomp.boot.eqtype]
contra_eqT [prf, in mathcomp.boot.eqtype]
contra_leq [prf, in mathcomp.boot.ssrnat]
contra_leq_ltn [prf, in mathcomp.boot.ssrnat]
contra_leq_not [prf, in mathcomp.boot.ssrnat]
contra_leqF [prf, in mathcomp.boot.ssrnat]
contra_leqN [prf, in mathcomp.boot.ssrnat]
contra_leqT [prf, in mathcomp.boot.ssrnat]
contra_ltn [prf, in mathcomp.boot.ssrnat]
contra_ltn_leq [prf, in mathcomp.boot.ssrnat]
contra_ltn_not [prf, in mathcomp.boot.ssrnat]
contra_ltnF [prf, in mathcomp.boot.ssrnat]
contra_ltnN [prf, in mathcomp.boot.ssrnat]
contra_ltnT [prf, in mathcomp.boot.ssrnat]
contra_neq [prf, in mathcomp.boot.eqtype]
contra_neq_eq [prf, in mathcomp.boot.eqtype]
contra_neq_not [prf, in mathcomp.boot.eqtype]
contra_neqF [prf, in mathcomp.boot.eqtype]
contra_neqN [prf, in mathcomp.boot.eqtype]
contra_neqT [prf, in mathcomp.boot.eqtype]
contra_not_eq [prf, in mathcomp.boot.eqtype]
contra_not_leq [prf, in mathcomp.boot.ssrnat]
contra_not_ltn [prf, in mathcomp.boot.ssrnat]
contra_not_neq [prf, in mathcomp.boot.eqtype]
contra_orbit [prf, in mathcomp.finite_group.action]
contraFeq [prf, in mathcomp.boot.eqtype]
contraFleq [prf, in mathcomp.boot.ssrnat]
contraFltn [prf, in mathcomp.boot.ssrnat]
contraFneq [prf, in mathcomp.boot.eqtype]
contraNeq [prf, in mathcomp.boot.eqtype]
contraNleq [prf, in mathcomp.boot.ssrnat]
contraNltn [prf, in mathcomp.boot.ssrnat]
contraNneq [prf, in mathcomp.boot.eqtype]
contraPeq [prf, in mathcomp.boot.eqtype]
contraPleq [prf, in mathcomp.boot.ssrnat]
contraPltn [prf, in mathcomp.boot.ssrnat]
contraPneq [prf, in mathcomp.boot.eqtype]
contraTeq [prf, in mathcomp.boot.eqtype]
contraTleq [prf, in mathcomp.boot.ssrnat]
contraTltn [prf, in mathcomp.boot.ssrnat]
contraTneq [prf, in mathcomp.boot.eqtype]
coord0 [prf, in mathcomp.algebra.vector]
coord_basis [prf, in mathcomp.algebra.vector]
coord_cfdot [prf, in mathcomp.group_representation.character]
coord_free [prf, in mathcomp.algebra.vector]
coord_is_scalar [prf, in mathcomp.algebra.vector]
coord_span [prf, in mathcomp.algebra.vector]
coord_sum_free [prf, in mathcomp.algebra.vector]
coord_vbasis [prf, in mathcomp.algebra.vector]
copid_mx_id [prf, in mathcomp.algebra.matrix]
coprime1n [prf, in mathcomp.boot.div]
coprime2n [prf, in mathcomp.boot.div]
coprime_abel_cent_TI [prf, in mathcomp.solvable.finmodule]
coprime_cardMg [prf, in mathcomp.finite_group.fingroup]
coprime_cent_mulG [prf, in mathcomp.solvable.hall]
coprime_comm_pcore [prf, in mathcomp.solvable.hall]
coprime_degree_support_cfcenter [prf, in mathcomp.group_representation.integral_char]
coprime_dvdl [prf, in mathcomp.boot.div]
coprime_dvdr [prf, in mathcomp.boot.div]
coprime_egcdn [prf, in mathcomp.boot.div]
coprime_Hall_exists [prf, in mathcomp.solvable.hall]
coprime_Hall_subset [prf, in mathcomp.solvable.hall]
coprime_Hall_trans [prf, in mathcomp.solvable.hall]
coprime_has_primes [prf, in mathcomp.boot.prime]
coprime_index_mulG [prf, in mathcomp.finite_group.fingroup]
coprime_modl [prf, in mathcomp.boot.div]
coprime_modr [prf, in mathcomp.boot.div]
coprime_morph [prf, in mathcomp.finite_group.quotient]
coprime_morphl [prf, in mathcomp.finite_group.quotient]
coprime_morphr [prf, in mathcomp.finite_group.quotient]
coprime_mulG_setI_norm [prf, in mathcomp.solvable.sylow]
coprime_mulGp_Hall [prf, in mathcomp.solvable.pgroup]
coprime_mulpG_Hall [prf, in mathcomp.solvable.pgroup]
coprime_norm_cent [prf, in mathcomp.solvable.hall]
coprime_norm_quotient_cent [prf, in mathcomp.solvable.hall]
coprime_num_den [prf, in mathcomp.algebra.rat]
coprime_p'group [prf, in mathcomp.solvable.pgroup]
coprime_partC [prf, in mathcomp.boot.prime]
coprime_pcoreC [prf, in mathcomp.solvable.pgroup]
coprime_pexpl [prf, in mathcomp.boot.div]
coprime_pexpr [prf, in mathcomp.boot.div]
coprime_pi' [prf, in mathcomp.boot.prime]
coprime_quotient_cent [prf, in mathcomp.solvable.hall]
coprime_sdprod_Hall_l [prf, in mathcomp.solvable.pgroup]
coprime_sdprod_Hall_r [prf, in mathcomp.solvable.pgroup]
coprime_sym [prf, in mathcomp.boot.div]
coprime_TIg [prf, in mathcomp.finite_group.fingroup]
coprimegS [prf, in mathcomp.finite_group.fingroup]
coprimeMl [prf, in mathcomp.boot.div]
coprimeMr [prf, in mathcomp.boot.div]
coprimen1 [prf, in mathcomp.boot.div]
coprimen2 [prf, in mathcomp.boot.div]
coprimenP [prf, in mathcomp.boot.div]
coprimenS [prf, in mathcomp.boot.div]
coprimeNz [prf, in mathcomp.algebra.intdiv]
coprimeP [prf, in mathcomp.boot.div]
coprimep_unit [prf, in mathcomp.field.qfpoly]
coprimePn [prf, in mathcomp.boot.div]
coprimeq_den [prf, in mathcomp.algebra.rat]
coprimeq_num [prf, in mathcomp.algebra.rat]
coprimeSg [prf, in mathcomp.finite_group.fingroup]
coprimeSn [prf, in mathcomp.boot.div]
coprimeXl [prf, in mathcomp.boot.div]
coprimeXr [prf, in mathcomp.boot.div]
coprimez_dvdl [prf, in mathcomp.algebra.intdiv]
coprimez_dvdr [prf, in mathcomp.algebra.intdiv]
coprimez_pexpl [prf, in mathcomp.algebra.intdiv]
coprimez_pexpr [prf, in mathcomp.algebra.intdiv]
coprimez_sym [prf, in mathcomp.algebra.intdiv]
coprimezE [prf, in mathcomp.algebra.intdiv]
coprimezMl [prf, in mathcomp.algebra.intdiv]
coprimezMr [prf, in mathcomp.algebra.intdiv]
coprimezN [prf, in mathcomp.algebra.intdiv]
coprimezP [prf, in mathcomp.algebra.intdiv]
coprimezXl [prf, in mathcomp.algebra.intdiv]
coprimezXr [prf, in mathcomp.algebra.intdiv]
cormen_lup_correct [prf, in mathcomp.algebra.matrix]
cormen_lup_detL [prf, in mathcomp.algebra.matrix]
cormen_lup_lower [prf, in mathcomp.algebra.matrix]
cormen_lup_perm [prf, in mathcomp.algebra.matrix]
cormen_lup_upper [prf, in mathcomp.algebra.matrix]
coset1 [prf, in mathcomp.finite_group.quotient]
coset1_injm [prf, in mathcomp.finite_group.quotient]
coset_default [prf, in mathcomp.finite_group.quotient]
coset_id [prf, in mathcomp.finite_group.quotient]
coset_idr [prf, in mathcomp.finite_group.quotient]
coset_invP [prf, in mathcomp.finite_group.quotient]
coset_kerl [prf, in mathcomp.finite_group.quotient]
coset_kerr [prf, in mathcomp.finite_group.quotient]
coset_mem [prf, in mathcomp.finite_group.quotient]
coset_morphM [prf, in mathcomp.finite_group.quotient]
coset_mulP [prf, in mathcomp.finite_group.quotient]
coset_norm [prf, in mathcomp.finite_group.quotient]
coset_one_proof [prf, in mathcomp.finite_group.quotient]
coset_oneP [prf, in mathcomp.finite_group.quotient]
coset_range_inv [prf, in mathcomp.finite_group.quotient]
coset_range_mul [prf, in mathcomp.finite_group.quotient]
coset_reprK [prf, in mathcomp.finite_group.quotient]
coset_splitting_field [prf, in mathcomp.group_representation.mxrepresentation]
cosetP [prf, in mathcomp.finite_group.quotient]
cosetpre1 [prf, in mathcomp.finite_group.quotient]
cosetpre_cent [prf, in mathcomp.finite_group.quotient]
cosetpre_cent1 [prf, in mathcomp.finite_group.quotient]
cosetpre_cent1s [prf, in mathcomp.finite_group.quotient]
cosetpre_cents [prf, in mathcomp.finite_group.quotient]
cosetpre_gen [prf, in mathcomp.finite_group.quotient]
cosetpre_maximal [prf, in mathcomp.solvable.gseries]
cosetpre_maximal_eq [prf, in mathcomp.solvable.gseries]
cosetpre_normal [prf, in mathcomp.finite_group.quotient]
cosetpre_proper [prf, in mathcomp.finite_group.quotient]
cosetpre_set1 [prf, in mathcomp.finite_group.quotient]
cosetpre_set1_coset [prf, in mathcomp.finite_group.quotient]
cosetpre_subcent [prf, in mathcomp.finite_group.quotient]
cosetpre_subcent1 [prf, in mathcomp.finite_group.quotient]
cosetpreK [prf, in mathcomp.finite_group.quotient]
cosetpreM [prf, in mathcomp.finite_group.quotient]
cosetpreSK [prf, in mathcomp.finite_group.quotient]
cotrigonalization [prf, in mathcomp.algebra.spectral]
cotrigonalization2 [prf, in mathcomp.algebra.spectral]
count_cat [prf, in mathcomp.boot.seq]
count_filter [prf, in mathcomp.boot.seq]
count_flatten [prf, in mathcomp.boot.seq]
count_logn_dprod_cycle [prf, in mathcomp.solvable.abelian]
count_map [prf, in mathcomp.boot.seq]
count_maskP [prf, in mathcomp.boot.seq]
count_mem_rem [prf, in mathcomp.boot.seq]
count_mem_uniq [prf, in mathcomp.boot.seq]
count_memPn [prf, in mathcomp.boot.seq]
count_merge [prf, in mathcomp.boot.path]
count_nseq [prf, in mathcomp.boot.seq]
count_pred0 [prf, in mathcomp.boot.seq]
count_predC [prf, in mathcomp.boot.seq]
count_predT [prf, in mathcomp.boot.seq]
count_predUI [prf, in mathcomp.boot.seq]
count_rem [prf, in mathcomp.boot.seq]
count_rev [prf, in mathcomp.boot.seq]
count_set_nth [prf, in mathcomp.boot.seq]
count_set_nth_ltn [prf, in mathcomp.boot.seq]
count_set_nthF [prf, in mathcomp.boot.seq]
count_size [prf, in mathcomp.boot.seq]
count_sort [prf, in mathcomp.boot.path]
count_subseqP [prf, in mathcomp.boot.seq]
count_undup [prf, in mathcomp.boot.seq]
count_uniq_mem [prf, in mathcomp.boot.seq]
countable_algebraic_closure [prf, in mathcomp.field.closed_field]
countable_field_extension [prf, in mathcomp.field.closed_field]
cover1 [prf, in mathcomp.boot.finset]
cover_imset [prf, in mathcomp.boot.finset]
cover_partition [prf, in mathcomp.boot.finset]
cover_setI [prf, in mathcomp.boot.finset]
coverD1 [prf, in mathcomp.boot.finset]
cpair1g_center [prf, in mathcomp.solvable.center]
cpair1g_dom [prf, in mathcomp.solvable.center]
cpair_center_id [prf, in mathcomp.solvable.center]
cpairg1_center [prf, in mathcomp.solvable.center]
cpairg1_dom [prf, in mathcomp.solvable.center]
cprod0g [prf, in mathcomp.finite_group.gproduct]
cprod1g [prf, in mathcomp.finite_group.gproduct]
cprod_abelem [prf, in mathcomp.solvable.abelian]
cprod_by_key [prf, in mathcomp.solvable.center]
cprod_by_uniq [prf, in mathcomp.solvable.center]
cprod_card_dprod [prf, in mathcomp.finite_group.gproduct]
cprod_center_id [prf, in mathcomp.solvable.center]
cprod_exponent [prf, in mathcomp.solvable.abelian]
cprod_extraspecial [prf, in mathcomp.solvable.maximal]
cprod_modl [prf, in mathcomp.finite_group.gproduct]
cprod_modr [prf, in mathcomp.finite_group.gproduct]
cprod_nil [prf, in mathcomp.solvable.nilpotent]
cprod_normal2 [prf, in mathcomp.finite_group.gproduct]
cprod_ntriv [prf, in mathcomp.finite_group.gproduct]
cprod_rowg [prf, in mathcomp.group_representation.mxabelem]
cprodA [prf, in mathcomp.finite_group.gproduct]
cprodC [prf, in mathcomp.finite_group.gproduct]
cprodE [prf, in mathcomp.finite_group.gproduct]
cprodEY [prf, in mathcomp.finite_group.gproduct]
cprodg1 [prf, in mathcomp.finite_group.gproduct]
cprodJ [prf, in mathcomp.finite_group.gproduct]
cprodm_actf [prf, in mathcomp.finite_group.gproduct]
cprodm_norm [prf, in mathcomp.finite_group.gproduct]
cprodm_sub [prf, in mathcomp.finite_group.gproduct]
cprodmE [prf, in mathcomp.finite_group.gproduct]
cprodmEl [prf, in mathcomp.finite_group.gproduct]
cprodmEr [prf, in mathcomp.finite_group.gproduct]
cprodP [prf, in mathcomp.finite_group.gproduct]
cprodW [prf, in mathcomp.finite_group.gproduct]
cprodWC [prf, in mathcomp.finite_group.gproduct]
cprodWpp [prf, in mathcomp.finite_group.gproduct]
cprodWY [prf, in mathcomp.finite_group.gproduct]
Crat0 [prf, in mathcomp.field.algC]
Crat1 [prf, in mathcomp.field.algC]
Crat_aut [prf, in mathcomp.field.algC]
Crat_divring_closed [prf, in mathcomp.field.algC]
Crat_rat [prf, in mathcomp.field.algC]
Crat_span_zmod_closed [prf, in mathcomp.field.algnum]
Crat_spanM [prf, in mathcomp.field.algnum]
Crat_spanP [prf, in mathcomp.field.algnum]
Crat_spanZ [prf, in mathcomp.field.algnum]
CratP [prf, in mathcomp.field.algC]
Creal_Crat [prf, in mathcomp.field.algC]
critical_class2 [prf, in mathcomp.solvable.maximal]
critical_extraspecial [prf, in mathcomp.solvable.maximal]
critical_p_stab_Aut [prf, in mathcomp.solvable.maximal]
curry_imset2l [prf, in mathcomp.boot.finset]
curry_imset2r [prf, in mathcomp.boot.finset]
curry_imset2X [prf, in mathcomp.boot.finset]
curry_mxvec_bij [prf, in mathcomp.algebra.matrix]
cV0Pn [prf, in mathcomp.algebra.matrix]
cycle1 [prf, in mathcomp.finite_group.fingroup]
cycle2g [prf, in mathcomp.finite_group.fingroup]
cycle_abelem [prf, in mathcomp.solvable.abelian]
cycle_abelian [prf, in mathcomp.finite_group.fingroup]
cycle_all2rel [prf, in mathcomp.boot.path]
cycle_all2rel_in [prf, in mathcomp.boot.path]
cycle_catC [prf, in mathcomp.boot.path]
cycle_constt [prf, in mathcomp.solvable.pgroup]
cycle_cyclic [prf, in mathcomp.solvable.cyclic]
cycle_eq1 [prf, in mathcomp.finite_group.fingroup]
cycle_from_next [prf, in mathcomp.boot.path]
cycle_from_prev [prf, in mathcomp.boot.path]
cycle_generator [prf, in mathcomp.solvable.cyclic]
cycle_id [prf, in mathcomp.finite_group.fingroup]
cycle_map [prf, in mathcomp.boot.path]
cycle_next [prf, in mathcomp.boot.path]
cycle_orbit [prf, in mathcomp.boot.fingraph]
cycle_orbit_cycle [prf, in mathcomp.boot.fingraph]
cycle_orbit_in [prf, in mathcomp.boot.fingraph]
cycle_path [prf, in mathcomp.boot.path]
cycle_prev [prf, in mathcomp.boot.path]
cycle_relI [prf, in mathcomp.boot.path]
cycle_repr_structure_pchar [prf, in mathcomp.group_representation.mxrepresentation]
cycle_sub_group [prf, in mathcomp.solvable.cyclic]
cycle_subG [prf, in mathcomp.finite_group.fingroup]
cycle_subgroup_char [prf, in mathcomp.solvable.cyclic]
cycle_traject [prf, in mathcomp.finite_group.fingroup]
cycleJ [prf, in mathcomp.finite_group.fingroup]
cycleM [prf, in mathcomp.solvable.cyclic]
cyclemM [prf, in mathcomp.solvable.cyclic]
cycleMsub [prf, in mathcomp.solvable.cyclic]
cycleP [prf, in mathcomp.finite_group.fingroup]
cyclePmin [prf, in mathcomp.finite_group.fingroup]
cycleV [prf, in mathcomp.finite_group.fingroup]
cycleX [prf, in mathcomp.finite_group.fingroup]
cyclic1 [prf, in mathcomp.solvable.cyclic]
cyclic_abelem_prime [prf, in mathcomp.solvable.abelian]
cyclic_abelian [prf, in mathcomp.solvable.cyclic]
cyclic_center_factor_abelian [prf, in mathcomp.solvable.center]
cyclic_dprod [prf, in mathcomp.solvable.cyclic]
cyclic_factor_abelian [prf, in mathcomp.solvable.center]
cyclic_metacyclic [prf, in mathcomp.solvable.cyclic]
cyclic_mx_eq0 [prf, in mathcomp.group_representation.mxrepresentation]
cyclic_mx_id [prf, in mathcomp.group_representation.mxrepresentation]
cyclic_mx_module [prf, in mathcomp.group_representation.mxrepresentation]
cyclic_mx_sub [prf, in mathcomp.group_representation.mxrepresentation]
cyclic_mxP [prf, in mathcomp.group_representation.mxrepresentation]
cyclic_nilpotent_quo_der1_cyclic [prf, in mathcomp.solvable.nilpotent]
cyclic_pgroup_Aut_structure [prf, in mathcomp.solvable.extremal]
cyclic_pgroup_dprod_trivg [prf, in mathcomp.solvable.abelian]
cyclic_SCN [prf, in mathcomp.solvable.extremal]
cyclic_small [prf, in mathcomp.solvable.cyclic]
cyclicJ [prf, in mathcomp.solvable.cyclic]
cyclicM [prf, in mathcomp.solvable.cyclic]
cyclicP [prf, in mathcomp.solvable.cyclic]
cyclicS [prf, in mathcomp.solvable.cyclic]
cyclicY [prf, in mathcomp.solvable.cyclic]
Cyclotomic0 [prf, in mathcomp.field.cyclotomic]
Cyclotomic_monic [prf, in mathcomp.field.cyclotomic]
cyclotomic_monic [prf, in mathcomp.field.cyclotomic]