mathcomp.ssreflect.tuple

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)

R (lemma)

ractE [in mathcomp.fingroup.action]
ractpermE [in mathcomp.fingroup.action]
ract_is_groupAction [in mathcomp.fingroup.action]
ract_is_action [in mathcomp.fingroup.action]
raddfMz [in mathcomp.algebra.ssrint]
raddf_int_scalable [in mathcomp.algebra.ssrint]
radmxE [in mathcomp.algebra.sesquilinear]
rad_ker [in mathcomp.algebra.sesquilinear]
rankJ [in mathcomp.solvable.abelian]
rankS [in mathcomp.solvable.abelian]
rank_mx_group [in mathcomp.character.mxabelem]
rank_Wedderburn_subring [in mathcomp.character.mxrepresentation]
rank_irr_comp [in mathcomp.character.mxrepresentation]
rank_irr1 [in mathcomp.character.mxrepresentation]
rank_cycle [in mathcomp.solvable.abelian]
rank_abelian_pgroup [in mathcomp.solvable.abelian]
rank_Ohm1 [in mathcomp.solvable.abelian]
rank_geP [in mathcomp.solvable.abelian]
rank_abelem [in mathcomp.solvable.abelian]
rank_Sylow [in mathcomp.solvable.abelian]
rank_pgroup [in mathcomp.solvable.abelian]
rank_witness [in mathcomp.solvable.abelian]
rank_gt0 [in mathcomp.solvable.abelian]
rank_ortho [in mathcomp.algebra.spectral]
rank_DnQ [in mathcomp.solvable.extraspecial]
rank_Dn [in mathcomp.solvable.extraspecial]
rank_orthomx [in mathcomp.algebra.sesquilinear]
rank_normal [in mathcomp.algebra.sesquilinear]
rank_mxdiag [in mathcomp.algebra.mxalgebra]
rank_diag_block_mx [in mathcomp.algebra.mxalgebra]
rank_row_0mx [in mathcomp.algebra.mxalgebra]
rank_row_mx0 [in mathcomp.algebra.mxalgebra]
rank_col_0mx [in mathcomp.algebra.mxalgebra]
rank_col_mx0 [in mathcomp.algebra.mxalgebra]
rank_copid_mx [in mathcomp.algebra.mxalgebra]
rank_pid_mx [in mathcomp.algebra.mxalgebra]
rank_ltmx [in mathcomp.algebra.mxalgebra]
rank_rV [in mathcomp.algebra.mxalgebra]
rank_leq_col [in mathcomp.algebra.mxalgebra]
rank_leq_row [in mathcomp.algebra.mxalgebra]
rank1 [in mathcomp.solvable.abelian]
ratArchimedean.is_intE [in mathcomp.algebra.rat]
ratArchimedean.is_natE [in mathcomp.algebra.rat]
ratArchimedean.truncP [in mathcomp.algebra.rat]
ratCK [in mathcomp.field.algC]
RatioP [in mathcomp.algebra.fraction]
Ratio_numden [in mathcomp.algebra.fraction]
Ratio0 [in mathcomp.algebra.fraction]
RatK [in mathcomp.algebra.rat]
ratP [in mathcomp.algebra.rat]
ratr_norm [in mathcomp.algebra.rat]
ratr_sg [in mathcomp.algebra.rat]
ratr_is_multiplicative [in mathcomp.algebra.rat]
ratr_is_additive [in mathcomp.algebra.rat]
ratr_nat [in mathcomp.algebra.rat]
ratr_int [in mathcomp.algebra.rat]
ratzD [in mathcomp.algebra.rat]
ratzE [in mathcomp.algebra.rat]
ratzM [in mathcomp.algebra.rat]
ratzN [in mathcomp.algebra.rat]
ratz_frac [in mathcomp.algebra.rat]
rat_poly_scale [in mathcomp.algebra.intdiv]
rat_algebraic_decidable [in mathcomp.field.algebraics_fundamentals]
rat_algebraic_archimedean [in mathcomp.field.algebraics_fundamentals]
rat_vm_compute [in mathcomp.algebra.rat]
rat_field_theory [in mathcomp.algebra.rat]
rat_ring_theory [in mathcomp.algebra.rat]
rat_linear [in mathcomp.algebra.rat]
rat_eq [in mathcomp.algebra.rat]
rat_eqE [in mathcomp.algebra.rat]
rat0 [in mathcomp.algebra.rat]
rat1 [in mathcomp.algebra.rat]
rcenter_normal [in mathcomp.character.mxrepresentation]
rcenter_group_set [in mathcomp.character.mxrepresentation]
rcent_map [in mathcomp.character.mxrepresentation]
rcent_quo [in mathcomp.character.mxrepresentation]
rcent_conj [in mathcomp.character.mxrepresentation]
rcent_eqg [in mathcomp.character.mxrepresentation]
rcent_subg [in mathcomp.character.mxrepresentation]
rcent_group_set [in mathcomp.character.mxrepresentation]
rcent_sub [in mathcomp.character.mxrepresentation]
rconj_mxJ [in mathcomp.character.mxrepresentation]
rconj_mxE [in mathcomp.character.mxrepresentation]
rconj_mx_repr [in mathcomp.character.mxrepresentation]
rcons_bseqP [in mathcomp.ssreflect.tuple]
rcons_tupleP [in mathcomp.ssreflect.tuple]
rcons_uniq [in mathcomp.ssreflect.seq]
rcons_injr [in mathcomp.ssreflect.seq]
rcons_injl [in mathcomp.ssreflect.seq]
rcons_inj [in mathcomp.ssreflect.seq]
rcons_cat [in mathcomp.ssreflect.seq]
rcons_cons [in mathcomp.ssreflect.seq]
rcons_path [in mathcomp.ssreflect.path]
rcons2_infix [in mathcomp.ssreflect.seq]
rcosetE [in mathcomp.fingroup.fingroup]
rcosetK [in mathcomp.fingroup.fingroup]
rcosetKV [in mathcomp.fingroup.fingroup]
rcosetM [in mathcomp.fingroup.fingroup]
rcosetP [in mathcomp.fingroup.fingroup]
rcosetS [in mathcomp.fingroup.fingroup]
rcosetsP [in mathcomp.fingroup.fingroup]
rcosets_cycle_transversal [in mathcomp.solvable.finmodule]
rcosets_cycle_partition [in mathcomp.solvable.finmodule]
rcosets_partition [in mathcomp.fingroup.fingroup]
rcosets_partition_mul [in mathcomp.fingroup.fingroup]
rcosets_id [in mathcomp.fingroup.fingroup]
rcoset_kercosetP [in mathcomp.fingroup.quotient]
rcoset_is_action [in mathcomp.fingroup.action]
rcoset_index2 [in mathcomp.fingroup.fingroup]
rcoset_mul [in mathcomp.fingroup.fingroup]
rcoset_repr [in mathcomp.fingroup.fingroup]
rcoset_id [in mathcomp.fingroup.fingroup]
rcoset_trans [in mathcomp.fingroup.fingroup]
rcoset_transl [in mathcomp.fingroup.fingroup]
rcoset_eqP [in mathcomp.fingroup.fingroup]
rcoset_sym [in mathcomp.fingroup.fingroup]
rcoset_refl [in mathcomp.fingroup.fingroup]
rcoset_inj [in mathcomp.fingroup.fingroup]
rcoset_kerP [in mathcomp.fingroup.morphism]
rcoset1 [in mathcomp.fingroup.fingroup]
realmxC [in mathcomp.algebra.spectral]
realmxD [in mathcomp.algebra.spectral]
realsym_hermsym [in mathcomp.algebra.spectral]
realz [in mathcomp.algebra.ssrint]
real_similar [in mathcomp.algebra.spectral]
reducible_Socle1 [in mathcomp.character.mxrepresentation]
reducible_Socle [in mathcomp.character.mxrepresentation]
regular_splittingAxiom [in mathcomp.field.galois]
regular_norm_coprime [in mathcomp.solvable.frobenius]
regular_norm_dvd_pred [in mathcomp.solvable.frobenius]
regular_op_inj [in mathcomp.character.mxrepresentation]
regular_module_ideal [in mathcomp.character.mxrepresentation]
regular_mx_faithful [in mathcomp.character.mxrepresentation]
regular_mx_repr [in mathcomp.character.mxrepresentation]
regular_vect_iso [in mathcomp.algebra.vector]
regular_fullv [in mathcomp.field.falgebra]
reindex [in mathcomp.ssreflect.bigop]
reindex_cfclass [in mathcomp.character.inertia]
reindex_acts [in mathcomp.fingroup.action]
reindex_astabs [in mathcomp.fingroup.action]
reindex_dprod [in mathcomp.character.classfun]
reindex_bigcprod [in mathcomp.fingroup.gproduct]
reindex_irr_class [in mathcomp.character.character]
reindex_inj [in mathcomp.ssreflect.bigop]
reindex_onto [in mathcomp.ssreflect.bigop]
reindex_omap [in mathcomp.ssreflect.bigop]
relpre_trans [in mathcomp.ssreflect.ssrbool]
relU_sym [in mathcomp.ssreflect.fingraph]
remE [in mathcomp.ssreflect.seq]
remgrM [in mathcomp.fingroup.gproduct]
remgrMid [in mathcomp.fingroup.gproduct]
remgrMl [in mathcomp.fingroup.gproduct]
remgrP [in mathcomp.fingroup.gproduct]
remgr_id [in mathcomp.fingroup.gproduct]
remgr1 [in mathcomp.fingroup.gproduct]
Remx_rect [in mathcomp.algebra.spectral]
rem_filter [in mathcomp.ssreflect.seq]
rem_mem [in mathcomp.ssreflect.seq]
rem_uniq [in mathcomp.ssreflect.seq]
rem_subseq [in mathcomp.ssreflect.seq]
rem_id [in mathcomp.ssreflect.seq]
rem_cons [in mathcomp.ssreflect.seq]
reprGLmM [in mathcomp.character.mxabelem]
reprK [in mathcomp.ssreflect.generic_quotient]
repr_coset_norm [in mathcomp.fingroup.quotient]
repr_coset1 [in mathcomp.fingroup.quotient]
repr_ofK [in mathcomp.ssreflect.generic_quotient]
repr_mem_transversal [in mathcomp.ssreflect.finset]
repr_mem_pblock [in mathcomp.ssreflect.finset]
repr_classesP [in mathcomp.fingroup.fingroup]
repr_class [in mathcomp.fingroup.fingroup]
repr_rcosetP [in mathcomp.fingroup.fingroup]
repr_group [in mathcomp.fingroup.fingroup]
repr_set0 [in mathcomp.fingroup.fingroup]
repr_set1 [in mathcomp.fingroup.fingroup]
repr_mx_free [in mathcomp.character.mxrepresentation]
repr_mxX [in mathcomp.character.mxrepresentation]
repr_mx_unitr [in mathcomp.character.mxrepresentation]
repr_mxVr [in mathcomp.character.mxrepresentation]
repr_mxMr [in mathcomp.character.mxrepresentation]
repr_mxV [in mathcomp.character.mxrepresentation]
repr_mx_unit [in mathcomp.character.mxrepresentation]
repr_mxKV [in mathcomp.character.mxrepresentation]
repr_mxK [in mathcomp.character.mxrepresentation]
repr_mxM [in mathcomp.character.mxrepresentation]
repr_mx1 [in mathcomp.character.mxrepresentation]
repr_irr_classK [in mathcomp.character.character]
repr_rsim_diag [in mathcomp.character.character]
reshapeKl [in mathcomp.ssreflect.seq]
reshapeKr [in mathcomp.ssreflect.seq]
reshape_leq [in mathcomp.ssreflect.seq]
reshape_indexK [in mathcomp.ssreflect.seq]
reshape_offsetP [in mathcomp.ssreflect.seq]
reshape_indexP [in mathcomp.ssreflect.seq]
reshape_rcons [in mathcomp.ssreflect.seq]
resize_mask [in mathcomp.ssreflect.seq]
restrict_aut_to_normal_num_field [in mathcomp.field.algnum]
restrict_aut_to_num_field [in mathcomp.field.algnum]
restrmEsub [in mathcomp.fingroup.morphism]
restrmP [in mathcomp.fingroup.morphism]
restrm_quotientE [in mathcomp.fingroup.quotient]
restr_perm_isom [in mathcomp.fingroup.action]
restr_perm_Aut [in mathcomp.fingroup.action]
restr_perm_commute [in mathcomp.fingroup.action]
restr_permE [in mathcomp.fingroup.action]
restr_perm_on [in mathcomp.fingroup.action]
restr_isom [in mathcomp.fingroup.morphism]
restr_isom_to [in mathcomp.fingroup.morphism]
resultant_eq0 [in mathcomp.algebra.mxpoly]
resultant_in_ideal [in mathcomp.algebra.mxpoly]
Res_sdprod_irr [in mathcomp.character.character]
Res_Iirr0 [in mathcomp.character.character]
Res_irr_neq0 [in mathcomp.character.character]
revK [in mathcomp.ssreflect.seq]
rev_bseqP [in mathcomp.ssreflect.tuple]
rev_tupleP [in mathcomp.ssreflect.tuple]
rev_reshape [in mathcomp.ssreflect.seq]
rev_flatten [in mathcomp.ssreflect.seq]
rev_zip [in mathcomp.ssreflect.seq]
rev_mask [in mathcomp.ssreflect.seq]
rev_rot [in mathcomp.ssreflect.seq]
rev_rotr [in mathcomp.ssreflect.seq]
rev_drop [in mathcomp.ssreflect.seq]
rev_take [in mathcomp.ssreflect.seq]
rev_pivot [in mathcomp.ssreflect.seq]
rev_uniq [in mathcomp.ssreflect.seq]
rev_nseq [in mathcomp.ssreflect.seq]
rev_rcons [in mathcomp.ssreflect.seq]
rev_cat [in mathcomp.ssreflect.seq]
rev_nilp [in mathcomp.ssreflect.seq]
rev_cons [in mathcomp.ssreflect.seq]
rev_sorted [in mathcomp.ssreflect.path]
rev_cycle [in mathcomp.ssreflect.path]
rev_path [in mathcomp.ssreflect.path]
rev_ord_inj [in mathcomp.ssreflect.fintype]
rev_ordK [in mathcomp.ssreflect.fintype]
rev_ord_proof [in mathcomp.ssreflect.fintype]
rev_big_rev [in mathcomp.ssreflect.bigop]
rfdP [in mathcomp.solvable.alt]
rfd_iso [in mathcomp.solvable.alt]
rfd_odd [in mathcomp.solvable.alt]
rfd_morph [in mathcomp.solvable.alt]
rfd_funP [in mathcomp.solvable.alt]
rfix_pgroup_char [in mathcomp.character.mxabelem]
rfix_abelem [in mathcomp.character.mxabelem]
rfix_regular [in mathcomp.character.mxrepresentation]
rfix_quo [in mathcomp.character.mxrepresentation]
rfix_conj [in mathcomp.character.mxrepresentation]
rfix_factmod [in mathcomp.character.mxrepresentation]
rfix_submod [in mathcomp.character.mxrepresentation]
rfix_morphim [in mathcomp.character.mxrepresentation]
rfix_morphpre [in mathcomp.character.mxrepresentation]
rfix_eqg [in mathcomp.character.mxrepresentation]
rfix_subg [in mathcomp.character.mxrepresentation]
rfix_mx_rstabC [in mathcomp.character.mxrepresentation]
rfix_mx_module [in mathcomp.character.mxrepresentation]
rfix_mx_conjsg [in mathcomp.character.mxrepresentation]
rfix_mxS [in mathcomp.character.mxrepresentation]
rfix_mx_id [in mathcomp.character.mxrepresentation]
rfix_mxP [in mathcomp.character.mxrepresentation]
rgdP [in mathcomp.solvable.alt]
rgraphK [in mathcomp.ssreflect.fingraph]
right_trans [in mathcomp.ssreflect.generic_quotient]
right_arc [in mathcomp.ssreflect.path]
ringmx_ind [in mathcomp.algebra.matrix]
ring_display [in mathcomp.algebra.ssrnum]
rkerP [in mathcomp.character.mxrepresentation]
rker_abelem [in mathcomp.character.mxabelem]
rker_map [in mathcomp.character.mxrepresentation]
rker_mx_rsim [in mathcomp.character.mxrepresentation]
rker_factmod [in mathcomp.character.mxrepresentation]
rker_submod [in mathcomp.character.mxrepresentation]
rker_quo [in mathcomp.character.mxrepresentation]
rker_conj [in mathcomp.character.mxrepresentation]
rker_morphim [in mathcomp.character.mxrepresentation]
rker_morphpre [in mathcomp.character.mxrepresentation]
rker_eqg [in mathcomp.character.mxrepresentation]
rker_subg [in mathcomp.character.mxrepresentation]
rker_linear [in mathcomp.character.mxrepresentation]
rker_normal [in mathcomp.character.mxrepresentation]
rker_norm [in mathcomp.character.mxrepresentation]
rmorphK [in mathcomp.algebra.sesquilinear]
rmorphMz [in mathcomp.algebra.ssrint]
rmorphXz [in mathcomp.algebra.ssrint]
rmorphzP [in mathcomp.algebra.ssrint]
rmorphZ_num [in mathcomp.field.algnum]
rmorph_int [in mathcomp.algebra.ssrint]
rmorph_unity_root [in mathcomp.algebra.poly]
rmorph_root [in mathcomp.algebra.poly]
rootC [in mathcomp.algebra.poly]
rootE [in mathcomp.algebra.poly]
rootM [in mathcomp.algebra.poly]
rootN [in mathcomp.algebra.poly]
rootP [in mathcomp.ssreflect.fingraph]
rootP [in mathcomp.algebra.poly]
rootPf [in mathcomp.algebra.poly]
rootPt [in mathcomp.algebra.poly]
roots_root [in mathcomp.ssreflect.fingraph]
roots_geq_poly_eq0 [in mathcomp.algebra.poly]
rootX [in mathcomp.algebra.poly]
rootZ [in mathcomp.algebra.poly]
root_cyclotomic [in mathcomp.field.cyclotomic]
root_minPoly_gal [in mathcomp.field.galois]
root_minCpoly [in mathcomp.field.algC]
root_small_adjoin_poly [in mathcomp.field.fieldext]
root_minPoly [in mathcomp.field.fieldext]
root_mxminpoly [in mathcomp.algebra.mxpoly]
root_annihilant [in mathcomp.algebra.polyXY]
root_monic_Aint [in mathcomp.field.algnum]
root_connect [in mathcomp.ssreflect.fingraph]
root_root [in mathcomp.ssreflect.fingraph]
root_ZXsubC [in mathcomp.algebra.poly]
root_exp_XsubC [in mathcomp.algebra.poly]
root_prod_XsubC [in mathcomp.algebra.poly]
root_exp [in mathcomp.algebra.poly]
root_comp [in mathcomp.algebra.poly]
root_polyC [in mathcomp.algebra.poly]
root_XaddC [in mathcomp.algebra.poly]
root_XsubC [in mathcomp.algebra.poly]
root_size_gt1 [in mathcomp.algebra.poly]
root0 [in mathcomp.algebra.poly]
root1 [in mathcomp.algebra.poly]
rotations_is_rot [in mathcomp.solvable.burnside_app]
rotD [in mathcomp.ssreflect.seq]
rotK [in mathcomp.ssreflect.seq]
rotrK [in mathcomp.ssreflect.seq]
rotr_bseqP [in mathcomp.ssreflect.tuple]
rotr_tupleP [in mathcomp.ssreflect.tuple]
rotr_rotr [in mathcomp.ssreflect.seq]
rotr_inj [in mathcomp.ssreflect.seq]
rotr_uniq [in mathcomp.ssreflect.seq]
rotr_size_cat [in mathcomp.ssreflect.seq]
rotr_ucycle [in mathcomp.ssreflect.path]
rotr_cycle [in mathcomp.ssreflect.path]
rotr1_rcons [in mathcomp.ssreflect.seq]
rotS [in mathcomp.ssreflect.seq]
rot_bseqP [in mathcomp.ssreflect.tuple]
rot_tupleP [in mathcomp.ssreflect.tuple]
rot_rotr [in mathcomp.ssreflect.seq]
rot_rot [in mathcomp.ssreflect.seq]
rot_rot_add [in mathcomp.ssreflect.seq]
rot_addC [in mathcomp.ssreflect.seq]
rot_minn [in mathcomp.ssreflect.seq]
rot_add_mod [in mathcomp.ssreflect.seq]
rot_to [in mathcomp.ssreflect.seq]
rot_index [in mathcomp.ssreflect.seq]
rot_uniq [in mathcomp.ssreflect.seq]
rot_inj [in mathcomp.ssreflect.seq]
rot_size_cat [in mathcomp.ssreflect.seq]
rot_size [in mathcomp.ssreflect.seq]
rot_oversize [in mathcomp.ssreflect.seq]
rot_to_arc [in mathcomp.ssreflect.path]
rot_ucycle [in mathcomp.ssreflect.path]
rot_cycle [in mathcomp.ssreflect.path]
rot_is_rot [in mathcomp.solvable.burnside_app]
rot_r1 [in mathcomp.solvable.burnside_app]
rot_eq_c0 [in mathcomp.solvable.burnside_app]
rot0 [in mathcomp.ssreflect.seq]
rot1_cons [in mathcomp.ssreflect.seq]
rowE [in mathcomp.algebra.matrix]
rowEsub [in mathcomp.algebra.matrix]
rowgD [in mathcomp.character.mxabelem]
rowgI [in mathcomp.character.mxabelem]
rowgK [in mathcomp.character.mxabelem]
rowgS [in mathcomp.character.mxabelem]
rowg_mxSK [in mathcomp.character.mxabelem]
rowg_mxK [in mathcomp.character.mxabelem]
rowg_mx_eq0 [in mathcomp.character.mxabelem]
rowg_mx1 [in mathcomp.character.mxabelem]
rowg_mxS [in mathcomp.character.mxabelem]
rowg_stable [in mathcomp.character.mxabelem]
rowg_group_set [in mathcomp.character.mxabelem]
rowg0 [in mathcomp.character.mxabelem]
rowg1 [in mathcomp.character.mxabelem]
rowK [in mathcomp.algebra.matrix]
rowKd [in mathcomp.algebra.matrix]
rowKu [in mathcomp.algebra.matrix]
rowP [in mathcomp.algebra.matrix]
rowsubE [in mathcomp.algebra.matrix]
rowsub_cast [in mathcomp.algebra.matrix]
rowsub_comp [in mathcomp.algebra.matrix]
rowsub_comp_sub [in mathcomp.algebra.mxalgebra]
rowsub_sub [in mathcomp.algebra.mxalgebra]
rowV0P [in mathcomp.algebra.mxalgebra]
rowV0Pn [in mathcomp.algebra.mxalgebra]
row_mxdiag [in mathcomp.algebra.matrix]
row_mxblock [in mathcomp.algebra.matrix]
row_mxcol [in mathcomp.algebra.matrix]
row_mxrow [in mathcomp.algebra.matrix]
row_diag_mx [in mathcomp.algebra.matrix]
row_sum_delta [in mathcomp.algebra.matrix]
row_permE [in mathcomp.algebra.matrix]
row_mul [in mathcomp.algebra.matrix]
row_mx_eq0 [in mathcomp.algebra.matrix]
row_mx0 [in mathcomp.algebra.matrix]
row_ind [in mathcomp.algebra.matrix]
row_row_mx [in mathcomp.algebra.matrix]
row_mxA [in mathcomp.algebra.matrix]
row_thin_mx [in mathcomp.algebra.matrix]
row_dsubmx [in mathcomp.algebra.matrix]
row_usubmx [in mathcomp.algebra.matrix]
row_mx_const [in mathcomp.algebra.matrix]
row_mxKr [in mathcomp.algebra.matrix]
row_mxEr [in mathcomp.algebra.matrix]
row_mxKl [in mathcomp.algebra.matrix]
row_mxEl [in mathcomp.algebra.matrix]
row_mx_key [in mathcomp.algebra.matrix]
row_rowsub [in mathcomp.algebra.matrix]
row_mxsub [in mathcomp.algebra.matrix]
row_eq [in mathcomp.algebra.matrix]
row_id [in mathcomp.algebra.matrix]
row_permEsub [in mathcomp.algebra.matrix]
row_permM [in mathcomp.algebra.matrix]
row_perm1 [in mathcomp.algebra.matrix]
row_const [in mathcomp.algebra.matrix]
row_matrixP [in mathcomp.algebra.matrix]
row_perm_const [in mathcomp.algebra.matrix]
row_perm_key [in mathcomp.algebra.matrix]
row_full_dom_hom [in mathcomp.character.mxrepresentation]
row_hom_mxP [in mathcomp.character.mxrepresentation]
row_schmidt_sub [in mathcomp.algebra.spectral]
row_unitarymxP [in mathcomp.algebra.spectral]
row_full_map [in mathcomp.algebra.mxalgebra]
row_free_map [in mathcomp.algebra.mxalgebra]
row_freePn [in mathcomp.algebra.mxalgebra]
row_free_castmx [in mathcomp.algebra.mxalgebra]
row_full_castmx [in mathcomp.algebra.mxalgebra]
row_base_free [in mathcomp.algebra.mxalgebra]
row_base0 [in mathcomp.algebra.mxalgebra]
row_full_unit [in mathcomp.algebra.mxalgebra]
row_free_unit [in mathcomp.algebra.mxalgebra]
row_free_inj [in mathcomp.algebra.mxalgebra]
row_freeP [in mathcomp.algebra.mxalgebra]
row_full_inj [in mathcomp.algebra.mxalgebra]
row_fullP [in mathcomp.algebra.mxalgebra]
row_subPn [in mathcomp.algebra.mxalgebra]
row_subP [in mathcomp.algebra.mxalgebra]
row_sub [in mathcomp.algebra.mxalgebra]
row_ebase_unit [in mathcomp.algebra.mxalgebra]
row_leq_rank [in mathcomp.algebra.mxalgebra]
row'Esub [in mathcomp.algebra.matrix]
row'Kd [in mathcomp.algebra.matrix]
row'Ku [in mathcomp.algebra.matrix]
row'_row_mx [in mathcomp.algebra.matrix]
row'_eq [in mathcomp.algebra.matrix]
row'_const [in mathcomp.algebra.matrix]
row'_col'_char_poly_mx [in mathcomp.algebra.mxpoly]
row0 [in mathcomp.algebra.matrix]
row1 [in mathcomp.algebra.matrix]
rpredMz [in mathcomp.algebra.ssrint]
rpredXsign [in mathcomp.algebra.ssrint]
rpredXz [in mathcomp.algebra.ssrint]
rpredZint [in mathcomp.algebra.ssrint]
rpred_Crat [in mathcomp.field.algC]
rpred_int [in mathcomp.algebra.ssrint]
rpred_rat [in mathcomp.algebra.rat]
rpred_horner [in mathcomp.algebra.poly]
rreg_div0 [in mathcomp.algebra.poly]
rreg_polyMC_eq0 [in mathcomp.algebra.poly]
rreg_size [in mathcomp.algebra.poly]
rreg_lead0 [in mathcomp.algebra.poly]
rreg_lead [in mathcomp.algebra.poly]
rshift_inj [in mathcomp.ssreflect.fintype]
rshift_subproof [in mathcomp.ssreflect.fintype]
rshift1 [in mathcomp.algebra.zmodp]
rsim_abelem_subg [in mathcomp.character.mxabelem]
rsim_irr_comp [in mathcomp.character.mxrepresentation]
rsim_regular_submod [in mathcomp.character.mxrepresentation]
rsim_regular_series [in mathcomp.character.mxrepresentation]
rsim_regular_factmod [in mathcomp.character.mxrepresentation]
rsim_submod1 [in mathcomp.character.mxrepresentation]
rstabS [in mathcomp.character.mxrepresentation]
rstabs_abelemG [in mathcomp.character.mxabelem]
rstabs_abelem [in mathcomp.character.mxabelem]
rstabs_map [in mathcomp.character.mxrepresentation]
rstabs_quo [in mathcomp.character.mxrepresentation]
rstabs_conj [in mathcomp.character.mxrepresentation]
rstabs_factmod [in mathcomp.character.mxrepresentation]
rstabs_submod [in mathcomp.character.mxrepresentation]
rstabs_morphim [in mathcomp.character.mxrepresentation]
rstabs_morphpre [in mathcomp.character.mxrepresentation]
rstabs_eqg [in mathcomp.character.mxrepresentation]
rstabs_subg [in mathcomp.character.mxrepresentation]
rstabs_act [in mathcomp.character.mxrepresentation]
rstabs_group_set [in mathcomp.character.mxrepresentation]
rstabs_sub [in mathcomp.character.mxrepresentation]
rstab_abelem [in mathcomp.character.mxabelem]
rstab_map [in mathcomp.character.mxrepresentation]
rstab_normal [in mathcomp.character.mxrepresentation]
rstab_norm [in mathcomp.character.mxrepresentation]
rstab_factmod [in mathcomp.character.mxrepresentation]
rstab_submod [in mathcomp.character.mxrepresentation]
rstab_act [in mathcomp.character.mxrepresentation]
rstab_quo [in mathcomp.character.mxrepresentation]
rstab_conj [in mathcomp.character.mxrepresentation]
rstab_morphim [in mathcomp.character.mxrepresentation]
rstab_morphpre [in mathcomp.character.mxrepresentation]
rstab_eqg [in mathcomp.character.mxrepresentation]
rstab_subg [in mathcomp.character.mxrepresentation]
rstab_group_set [in mathcomp.character.mxrepresentation]
rstab_sub [in mathcomp.character.mxrepresentation]
rsubmxEsub [in mathcomp.algebra.matrix]
rsubmx_key [in mathcomp.algebra.matrix]
rVabelemD [in mathcomp.character.mxabelem]
rVabelemJ [in mathcomp.character.mxabelem]
rVabelemK [in mathcomp.character.mxabelem]
rVabelemN [in mathcomp.character.mxabelem]
rVabelemS [in mathcomp.character.mxabelem]
rVabelemZ [in mathcomp.character.mxabelem]
rVabelem_minj [in mathcomp.character.mxabelem]
rVabelem_mK [in mathcomp.character.mxabelem]
rVabelem_injm [in mathcomp.character.mxabelem]
rVabelem_inj [in mathcomp.character.mxabelem]
rVabelem0 [in mathcomp.character.mxabelem]
rVnpolyK [in mathcomp.algebra.qpoly]
rVpolyK [in mathcomp.algebra.mxpoly]
rVpoly_is_linear [in mathcomp.algebra.mxpoly]
rVpoly_delta [in mathcomp.algebra.mxpoly]
rV_abelem_sJ [in mathcomp.character.mxabelem]
rV_form0_eq0 [in mathcomp.algebra.sesquilinear]
rV_formee [in mathcomp.algebra.sesquilinear]
rV_eqP [in mathcomp.algebra.mxalgebra]
rV_subP [in mathcomp.algebra.mxalgebra]
rV0Pn [in mathcomp.algebra.matrix]
R012_inj [in mathcomp.solvable.burnside_app]
R013_inj [in mathcomp.solvable.burnside_app]
R021_inj [in mathcomp.solvable.burnside_app]
R024_inj [in mathcomp.solvable.burnside_app]
R031_inj [in mathcomp.solvable.burnside_app]
R034_inj [in mathcomp.solvable.burnside_app]
R042_inj [in mathcomp.solvable.burnside_app]
R043_inj [in mathcomp.solvable.burnside_app]
r05_inv [in mathcomp.solvable.burnside_app]
R05_inj [in mathcomp.solvable.burnside_app]
r1_inv [in mathcomp.solvable.burnside_app]
R1_inj [in mathcomp.solvable.burnside_app]
r14_inv [in mathcomp.solvable.burnside_app]
R14_inj [in mathcomp.solvable.burnside_app]
r2_inv [in mathcomp.solvable.burnside_app]
R2_inj [in mathcomp.solvable.burnside_app]
R23_inj [in mathcomp.solvable.burnside_app]
r3_inv [in mathcomp.solvable.burnside_app]
R3_inj [in mathcomp.solvable.burnside_app]
R32_inj [in mathcomp.solvable.burnside_app]
r41_inv [in mathcomp.solvable.burnside_app]
R41_inj [in mathcomp.solvable.burnside_app]
r50_inv [in mathcomp.solvable.burnside_app]
R50_inj [in mathcomp.solvable.burnside_app]

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)