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 | _ | other | (14626 entries) |

Projection 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 | _ | other | (165 entries) |

Record 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 | _ | other | (112 entries) |

Lemma 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 | _ | other | (7292 entries) |

Section 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 | _ | other | (761 entries) |

Constructor 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 | _ | other | (250 entries) |

Abbreviation 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 | _ | other | (390 entries) |

Inductive 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 | _ | other | (84 entries) |

Definition 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 | _ | other | (3144 entries) |

Module 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 | _ | other | (126 entries) |

Axiom 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 | _ | other | (28 entries) |

Variable 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 | _ | other | (2221 entries) |

Library 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 | _ | other | (53 entries) |

## R

r [definition, in extremal]r [definition, in extremal]

r [definition, in extremal]

r [abbreviation, in mxabelem]

ract [definition, in action]

ractE [lemma, in action]

raction [definition, in action]

ractpermE [lemma, in action]

ract_is_groupAction [lemma, in action]

ract_groupAction [definition, in action]

ract_is_action [lemma, in action]

range [abbreviation, in action]

rank [definition, in abelian]

rankJ [lemma, in abelian]

rankS [lemma, in abelian]

rank_pid_mx [lemma, in mxalgebra]

rank_leq_row [lemma, in mxalgebra]

rank_irr_comp [lemma, in mxrepresentation]

rank_Dn [lemma, in extraspecial]

rank_DnQ [lemma, in extraspecial]

rank_Ohm1 [lemma, in abelian]

rank_Sylow [lemma, in abelian]

rank_pgroup [lemma, in abelian]

rank_gt0 [lemma, in abelian]

rank_copid_mx [lemma, in mxalgebra]

rank_leq_col [lemma, in mxalgebra]

rank_abelem [lemma, in abelian]

rank_witness [lemma, in abelian]

rank_irr1 [lemma, in mxrepresentation]

rank_cycle [lemma, in abelian]

rank_abelian_pgroup [lemma, in abelian]

rank_geP [lemma, in abelian]

rank_ltmx [lemma, in mxalgebra]

rank_Wedderburn_subring [lemma, in mxrepresentation]

rank_rV [lemma, in mxalgebra]

rank1 [lemma, in abelian]

RawAction [section, in action]

RawAction.ActsSetop [section, in action]

RawAction.ActsSetop.A [variable, in action]

RawAction.ActsSetop.AactS [variable, in action]

RawAction.ActsSetop.AactT [variable, in action]

RawAction.ActsSetop.S [variable, in action]

RawAction.ActsSetop.T [variable, in action]

RawAction.aT [variable, in action]

RawAction.D [variable, in action]

RawAction.Reindex [section, in action]

RawAction.Reindex.idx [variable, in action]

RawAction.Reindex.op [variable, in action]

RawAction.Reindex.S [variable, in action]

RawAction.Reindex.vT [variable, in action]

RawAction.rT [variable, in action]

RawAction.to [variable, in action]

RawGroupAction [section, in action]

RawGroupAction.a [variable, in action]

RawGroupAction.A [variable, in action]

RawGroupAction.aT [variable, in action]

RawGroupAction.B [variable, in action]

RawGroupAction.D [variable, in action]

RawGroupAction.Da [variable, in action]

RawGroupAction.R [variable, in action]

RawGroupAction.rT [variable, in action]

RawGroupAction.S [variable, in action]

RawGroupAction.sAD [variable, in action]

RawGroupAction.sSR [variable, in action]

RawGroupAction.to [variable, in action]

rcent [definition, in mxrepresentation]

rcent_group_set [lemma, in mxrepresentation]

rcent_quo [lemma, in mxrepresentation]

rcent_eqg [lemma, in mxrepresentation]

rcent_group [definition, in mxrepresentation]

rcent_subg [lemma, in mxrepresentation]

rcent_sub [lemma, in mxrepresentation]

rcent_map [lemma, in mxrepresentation]

rcent_conj [lemma, in mxrepresentation]

rconj_mxE [lemma, in mxrepresentation]

rconj_repr [definition, in mxrepresentation]

rconj_mxJ [lemma, in mxrepresentation]

rconj_mx [definition, in mxrepresentation]

rconj_mx_repr [lemma, in mxrepresentation]

rcons [definition, in seq]

rcons_uniq [lemma, in seq]

rcons_cat [lemma, in seq]

rcons_cons [lemma, in seq]

rcoset [definition, in fingroup]

rcosetE [lemma, in fingroup]

rcosetK [lemma, in fingroup]

rcosetKV [lemma, in fingroup]

rcosetM [lemma, in fingroup]

rcosetP [lemma, in fingroup]

RcosetPcycleTransversalWitness [constructor, in finmodule]

RcosetReprSpec [constructor, in fingroup]

rcosets [definition, in fingroup]

rcosetS [lemma, in fingroup]

rcosetsP [lemma, in fingroup]

rcosets_pcycle_transversal [definition, in finmodule]

rcosets_pcycle_transversal_witness [inductive, in finmodule]

rcosets_pcycle_transversal_exists [lemma, in finmodule]

rcoset_kercosetP [lemma, in quotient]

rcoset_repr [lemma, in fingroup]

rcoset_transl [lemma, in fingroup]

rcoset_sym [lemma, in fingroup]

rcoset_id [lemma, in fingroup]

rcoset_inj [lemma, in fingroup]

rcoset_repr_spec [inductive, in fingroup]

rcoset_is_action [lemma, in action]

rcoset_action [definition, in action]

rcoset_refl [lemma, in fingroup]

rcoset_mul [lemma, in fingroup]

rcoset_index2 [lemma, in fingroup]

rcoset_trans [lemma, in fingroup]

rcoset_kerP [lemma, in morphism]

rcoset_transr [lemma, in fingroup]

rcoset1 [lemma, in fingroup]

reducebig [definition, in bigop]

reducible_Socle [lemma, in mxrepresentation]

reducible_Socle1 [lemma, in mxrepresentation]

reflect [inductive, in ssrbool]

Reflect [section, in ssrbool]

ReflectConnectives [section, in ssrbool]

ReflectConnectives.b1 [variable, in ssrbool]

ReflectConnectives.b2 [variable, in ssrbool]

ReflectConnectives.b3 [variable, in ssrbool]

ReflectConnectives.b4 [variable, in ssrbool]

ReflectConnectives.b5 [variable, in ssrbool]

ReflectCore [section, in ssrbool]

ReflectCore.b [variable, in ssrbool]

ReflectCore.c [variable, in ssrbool]

ReflectCore.Hb [variable, in ssrbool]

ReflectCore.P [variable, in ssrbool]

ReflectCore.Q [variable, in ssrbool]

ReflectF [constructor, in ssrbool]

ReflectNegCore [section, in ssrbool]

ReflectNegCore.b [variable, in ssrbool]

ReflectNegCore.c [variable, in ssrbool]

ReflectNegCore.Hb [variable, in ssrbool]

ReflectNegCore.P [variable, in ssrbool]

ReflectNegCore.Q [variable, in ssrbool]

ReflectProp [section, in morphism]

ReflectProp.aT [variable, in morphism]

ReflectProp.Defs [section, in morphism]

ReflectProp.Defs.A [variable, in morphism]

ReflectProp.Defs.B [variable, in morphism]

ReflectProp.Defs.MorphicProps [section, in morphism]

ReflectProp.Defs.MorphicProps.f [variable, in morphism]

ReflectProp.f [variable, in morphism]

ReflectProp.G [variable, in morphism]

ReflectProp.Main [section, in morphism]

ReflectProp.Main.G [variable, in morphism]

ReflectProp.Main.H [variable, in morphism]

ReflectProp.rT [variable, in morphism]

ReflectT [constructor, in ssrbool]

Reflect.b [variable, in ssrbool]

Reflect.b' [variable, in ssrbool]

Reflect.c [variable, in ssrbool]

Reflect.P [variable, in ssrbool]

Reflect.Pb [variable, in ssrbool]

Reflect.Pb' [variable, in ssrbool]

Reflect.Q [variable, in ssrbool]

reflexive [definition, in ssrbool]

regular_mx [definition, in mxrepresentation]

regular_repr [definition, in mxrepresentation]

regular_op_inj [lemma, in mxrepresentation]

regular_norm_coprime [lemma, in frobenius]

regular_mx_repr [lemma, in mxrepresentation]

regular_module_ideal [lemma, in mxrepresentation]

regular_norm_dvd_pred [lemma, in frobenius]

regular_mx_faithful [lemma, in mxrepresentation]

reindex [lemma, in bigop]

reindex_inj [lemma, in bigop]

reindex_astabs [lemma, in action]

reindex_acts [lemma, in action]

reindex_onto [lemma, in bigop]

rel [definition, in ssrbool]

RelAdjunction [section, in fingraph]

RelAdjunction [constructor, in fingraph]

RelAdjunction.a [variable, in fingraph]

RelAdjunction.e [variable, in fingraph]

RelAdjunction.e' [variable, in fingraph]

RelAdjunction.h [variable, in fingraph]

RelAdjunction.Ha [variable, in fingraph]

RelAdjunction.He [variable, in fingraph]

RelAdjunction.He' [variable, in fingraph]

RelAdjunction.T [variable, in fingraph]

RelAdjunction.T' [variable, in fingraph]

RelationProperties [section, in ssrbool]

RelationProperties.R [variable, in ssrbool]

RelationProperties.T [variable, in ssrbool]

relU [definition, in ssrbool]

relU_sym [lemma, in fingraph]

rel_unit [projection, in fingraph]

rel_base [definition, in path]

rel_functor [projection, in fingraph]

rel_of_simpl_rel [definition, in ssrbool]

rel_adjunction [record, in fingraph]

remgr [definition, in gproduct]

remgrM [lemma, in gproduct]

remgrMid [lemma, in gproduct]

remgrMl [lemma, in gproduct]

remgrP [lemma, in gproduct]

remgr_id [lemma, in gproduct]

remgr1 [lemma, in gproduct]

repr [definition, in fingroup]

Repr [section, in fingroup]

reprG [abbreviation, in mxrepresentation]

reprGLm [definition, in mxabelem]

reprGLmM [lemma, in mxabelem]

reprGL_morphism [definition, in mxabelem]

repr_coset1 [lemma, in quotient]

repr_group [lemma, in fingroup]

repr_mxMr [lemma, in mxrepresentation]

repr_class [lemma, in fingroup]

repr_rcosetP [lemma, in fingroup]

repr_set0 [lemma, in fingroup]

repr_coset_norm [lemma, in quotient]

repr_mxV [lemma, in mxrepresentation]

repr_mx [projection, in mxrepresentation]

repr_mxVr [lemma, in mxrepresentation]

repr_set1 [lemma, in fingroup]

repr_mx_unit [lemma, in mxrepresentation]

repr_mxKV [lemma, in mxrepresentation]

repr_mxM [lemma, in mxrepresentation]

repr_mx1 [lemma, in mxrepresentation]

repr_mxK [lemma, in mxrepresentation]

repr_mxX [lemma, in mxrepresentation]

repr_mx_unitr [lemma, in mxrepresentation]

repr_mx_free [lemma, in mxrepresentation]

Repr.gT [variable, in fingroup]

reshape [definition, in seq]

reshapeKl [lemma, in seq]

reshapeKr [lemma, in seq]

Restrict [section, in alt]

Restrict [section, in action]

RestrictActionTheory [section, in action]

RestrictActionTheory.A [variable, in action]

RestrictActionTheory.aT [variable, in action]

RestrictActionTheory.D [variable, in action]

RestrictActionTheory.rT [variable, in action]

RestrictActionTheory.sAD [variable, in action]

RestrictActionTheory.to [variable, in action]

RestrictedMorphism [section, in morphism]

RestrictedMorphism.A [variable, in morphism]

RestrictedMorphism.aT [variable, in morphism]

RestrictedMorphism.D [variable, in morphism]

RestrictedMorphism.Props [section, in morphism]

RestrictedMorphism.Props.f [variable, in morphism]

RestrictedMorphism.Props.sAD [variable, in morphism]

RestrictedMorphism.rT [variable, in morphism]

RestrictPerm [section, in action]

RestrictPerm.S [variable, in action]

RestrictPerm.T [variable, in action]

Restrict.A [variable, in action]

Restrict.aT [variable, in action]

Restrict.card_T [variable, in alt]

Restrict.D [variable, in action]

Restrict.rT [variable, in action]

Restrict.sAD [variable, in action]

Restrict.T [variable, in alt]

Restrict.to [variable, in action]

Restrict.x [variable, in alt]

restrm [definition, in morphism]

restrmP [lemma, in morphism]

restrm_morphism [definition, in morphism]

restr_perm_on [lemma, in action]

restr_perm [definition, in action]

restr_perm_isom [lemma, in action]

restr_perm_morphism [definition, in action]

restr_perm_Aut [lemma, in action]

restr_permE [lemma, in action]

resultant [definition, in mxpoly]

Resultant [section, in mxpoly]

resultant_eq0 [lemma, in mxpoly]

Resultant.F [variable, in mxpoly]

Resultant.p [variable, in mxpoly]

Resultant.q [variable, in mxpoly]

returnType [definition, in ssreflect]

rev [definition, in seq]

Rev [section, in seq]

revK [lemma, in seq]

rev_cons [lemma, in seq]

rev_tuple [definition, in tuple]

rev_tupleP [lemma, in tuple]

rev_ord_inj [lemma, in fintype]

rev_rcons [lemma, in seq]

rev_ordK [lemma, in fintype]

rev_ord_proof [lemma, in fintype]

rev_ord [definition, in fintype]

rev_rotr [lemma, in seq]

rev_trans [lemma, in ssrbool]

rev_uniq [lemma, in seq]

rev_right_loop [definition, in ssrfun]

rev_left_loop [definition, in ssrfun]

rev_rot [lemma, in seq]

rev_cat [lemma, in seq]

Rev.T [variable, in seq]

rF [abbreviation, in mxrepresentation]

rfd [definition, in alt]

rfdP [lemma, in alt]

rfd_morph [lemma, in alt]

rfd_iso [lemma, in alt]

rfd_funP [lemma, in alt]

rfd_odd [lemma, in alt]

rfd_fun [definition, in alt]

rfd_morphism [definition, in alt]

rfix_conj [lemma, in mxrepresentation]

rfix_mx_id [lemma, in mxrepresentation]

rfix_subg [lemma, in mxrepresentation]

rfix_regular [lemma, in mxrepresentation]

rfix_mxS [lemma, in mxrepresentation]

rfix_mx_rstabC [lemma, in mxrepresentation]

rfix_mx_conjsg [lemma, in mxrepresentation]

rfix_submod [lemma, in mxrepresentation]

rfix_factmod [lemma, in mxrepresentation]

rfix_pgroup_char [lemma, in mxabelem]

rfix_mxP [lemma, in mxrepresentation]

rfix_abelem [lemma, in mxabelem]

rfix_morphpre [lemma, in mxrepresentation]

rfix_mx [definition, in mxrepresentation]

rfix_quo [lemma, in mxrepresentation]

rfix_morphim [lemma, in mxrepresentation]

rfix_eqg [lemma, in mxrepresentation]

rfix_mx_module [lemma, in mxrepresentation]

rG [definition, in mxabelem]

rG [abbreviation, in mxrepresentation]

rG [abbreviation, in mxrepresentation]

rGB [abbreviation, in mxrepresentation]

rGB [abbreviation, in mxrepresentation]

rgd [definition, in alt]

rgdP [lemma, in alt]

rgd_fun [definition, in alt]

rGf [abbreviation, in mxrepresentation]

rGf [abbreviation, in mxrepresentation]

rGf [abbreviation, in mxrepresentation]

rGf [abbreviation, in mxrepresentation]

rGH [abbreviation, in mxrepresentation]

rGH [abbreviation, in mxrepresentation]

rH [abbreviation, in mxrepresentation]

rH [abbreviation, in mxrepresentation]

rH [abbreviation, in mxrepresentation]

rH [abbreviation, in mxrepresentation]

rH [definition, in mxrepresentation]

rhs [definition, in finset]

right_arc [lemma, in path]

right_id [definition, in ssrfun]

right_distributive [definition, in ssrfun]

right_loop [definition, in ssrfun]

right_inverse [definition, in ssrfun]

right_zero [definition, in ssrfun]

right_commutative [definition, in ssrfun]

right_transitive [definition, in ssrbool]

right_injective [definition, in ssrfun]

right_mx_ideal [definition, in mxalgebra]

Ring [section, in poly]

Ring [module, in ssralg]

Ring [module, in finalg]

RingRepr [section, in mxrepresentation]

RingRepr.ChangeGroup [section, in mxrepresentation]

RingRepr.ChangeGroup.G [variable, in mxrepresentation]

RingRepr.ChangeGroup.gT [variable, in mxrepresentation]

RingRepr.ChangeGroup.H [variable, in mxrepresentation]

RingRepr.ChangeGroup.n [variable, in mxrepresentation]

RingRepr.ChangeGroup.rG [variable, in mxrepresentation]

RingRepr.ChangeGroup.SameGroup [section, in mxrepresentation]

RingRepr.ChangeGroup.SameGroup.eqGH [variable, in mxrepresentation]

RingRepr.ChangeGroup.SameGroup.Stabiliser [section, in mxrepresentation]

RingRepr.ChangeGroup.SameGroup.Stabiliser.m [variable, in mxrepresentation]

RingRepr.ChangeGroup.SameGroup.Stabiliser.U [variable, in mxrepresentation]

RingRepr.ChangeGroup.SubGroup [section, in mxrepresentation]

RingRepr.ChangeGroup.SubGroup.sHG [variable, in mxrepresentation]

RingRepr.ChangeGroup.SubGroup.Stabiliser [section, in mxrepresentation]

RingRepr.ChangeGroup.SubGroup.Stabiliser.m [variable, in mxrepresentation]

RingRepr.ChangeGroup.SubGroup.Stabiliser.U [variable, in mxrepresentation]

RingRepr.Conjugate [section, in mxrepresentation]

RingRepr.Conjugate.B [variable, in mxrepresentation]

RingRepr.Conjugate.G [variable, in mxrepresentation]

RingRepr.Conjugate.gT [variable, in mxrepresentation]

RingRepr.Conjugate.n [variable, in mxrepresentation]

RingRepr.Conjugate.rG [variable, in mxrepresentation]

RingRepr.Conjugate.uB [variable, in mxrepresentation]

RingRepr.Morphim [section, in mxrepresentation]

RingRepr.Morphim.aT [variable, in mxrepresentation]

RingRepr.Morphim.D [variable, in mxrepresentation]

RingRepr.Morphim.f [variable, in mxrepresentation]

RingRepr.Morphim.G [variable, in mxrepresentation]

RingRepr.Morphim.n [variable, in mxrepresentation]

RingRepr.Morphim.rGf [variable, in mxrepresentation]

RingRepr.Morphim.rT [variable, in mxrepresentation]

RingRepr.Morphim.sGD [variable, in mxrepresentation]

RingRepr.Morphim.Stabiliser [section, in mxrepresentation]

RingRepr.Morphim.Stabiliser.m [variable, in mxrepresentation]

RingRepr.Morphim.Stabiliser.U [variable, in mxrepresentation]

RingRepr.Morphpre [section, in mxrepresentation]

RingRepr.Morphpre.aT [variable, in mxrepresentation]

RingRepr.Morphpre.D [variable, in mxrepresentation]

RingRepr.Morphpre.f [variable, in mxrepresentation]

RingRepr.Morphpre.G [variable, in mxrepresentation]

RingRepr.Morphpre.n [variable, in mxrepresentation]

RingRepr.Morphpre.rG [variable, in mxrepresentation]

RingRepr.Morphpre.rT [variable, in mxrepresentation]

RingRepr.Morphpre.Stabiliser [section, in mxrepresentation]

RingRepr.Morphpre.Stabiliser.m [variable, in mxrepresentation]

RingRepr.Morphpre.Stabiliser.U [variable, in mxrepresentation]

RingRepr.OneRepresentation [section, in mxrepresentation]

RingRepr.OneRepresentation.CentHom [section, in mxrepresentation]

RingRepr.OneRepresentation.CentHom.f [variable, in mxrepresentation]

RingRepr.OneRepresentation.G [variable, in mxrepresentation]

RingRepr.OneRepresentation.gT [variable, in mxrepresentation]

RingRepr.OneRepresentation.n [variable, in mxrepresentation]

RingRepr.OneRepresentation.rG [variable, in mxrepresentation]

RingRepr.OneRepresentation.Stabiliser [section, in mxrepresentation]

RingRepr.OneRepresentation.Stabiliser.m [variable, in mxrepresentation]

RingRepr.OneRepresentation.Stabiliser.U [variable, in mxrepresentation]

RingRepr.Proper [section, in mxrepresentation]

RingRepr.Proper.G [variable, in mxrepresentation]

RingRepr.Proper.gT [variable, in mxrepresentation]

RingRepr.Proper.n' [variable, in mxrepresentation]

RingRepr.Proper.rG [variable, in mxrepresentation]

RingRepr.Quotient [section, in mxrepresentation]

RingRepr.Quotient.G [variable, in mxrepresentation]

RingRepr.Quotient.gT [variable, in mxrepresentation]

RingRepr.Quotient.n [variable, in mxrepresentation]

RingRepr.Quotient.rG [variable, in mxrepresentation]

RingRepr.Quotient.SubQuotient [section, in mxrepresentation]

RingRepr.Quotient.SubQuotient.H [variable, in mxrepresentation]

RingRepr.Quotient.SubQuotient.krH [variable, in mxrepresentation]

RingRepr.Quotient.SubQuotient.nHG [variable, in mxrepresentation]

RingRepr.R [variable, in mxrepresentation]

RingRepr.Regular [section, in mxrepresentation]

RingRepr.Regular.G [variable, in mxrepresentation]

RingRepr.Regular.GringMx [section, in mxrepresentation]

RingRepr.Regular.GringMx.n [variable, in mxrepresentation]

RingRepr.Regular.GringMx.rG [variable, in mxrepresentation]

RingRepr.Regular.GringOp [section, in mxrepresentation]

RingRepr.Regular.GringOp.n [variable, in mxrepresentation]

RingRepr.Regular.GringOp.rG [variable, in mxrepresentation]

RingRepr.Regular.gT [variable, in mxrepresentation]

Ring.R [variable, in poly]

rker [definition, in mxrepresentation]

rkerP [lemma, in mxrepresentation]

rker_quo [lemma, in mxrepresentation]

rker_subg [lemma, in mxrepresentation]

rker_morphim [lemma, in mxrepresentation]

rker_mx_rsim [lemma, in mxrepresentation]

rker_norm [lemma, in mxrepresentation]

rker_linear [lemma, in mxrepresentation]

rker_group [definition, in mxrepresentation]

rker_abelem [lemma, in mxabelem]

rker_factmod [lemma, in mxrepresentation]

rker_normal [lemma, in mxrepresentation]

rker_map [lemma, in mxrepresentation]

rker_eqg [lemma, in mxrepresentation]

rker_conj [lemma, in mxrepresentation]

rker_submod [lemma, in mxrepresentation]

rker_morphpre [lemma, in mxrepresentation]

RMorphism [module, in ssralg]

rmorph_unity_root [lemma, in poly]

root [definition, in fingraph]

root [definition, in poly]

rootP [lemma, in fingraph]

roots [definition, in fingraph]

roots_root [lemma, in fingraph]

root_root [lemma, in fingraph]

root_connect [lemma, in fingraph]

root_factor_theorem [lemma, in poly]

root_field_map_poly [lemma, in poly]

root_of_unity [definition, in poly]

root_map_poly [lemma, in poly]

root_prod_factors [lemma, in poly]

rot [definition, in seq]

RotCompLemmas [section, in seq]

RotCompLemmas.T [variable, in seq]

rotK [lemma, in seq]

rotr [definition, in seq]

rotrK [lemma, in seq]

RotrLemmas [section, in seq]

RotrLemmas.n0 [variable, in seq]

RotrLemmas.T [variable, in seq]

RotrLemmas.T' [variable, in seq]

rotr_tuple [definition, in tuple]

rotr_inj [lemma, in seq]

rotr_uniq [lemma, in seq]

rotr_size_cat [lemma, in seq]

rotr_rotr [lemma, in seq]

rotr_tupleP [lemma, in tuple]

rotr1_rcons [lemma, in seq]

rotS [lemma, in seq]

RotToArcSpec [constructor, in path]

RotToSpec [constructor, in seq]

rot_inj [lemma, in seq]

rot_tuple [definition, in tuple]

rot_size [lemma, in seq]

rot_to_spec [inductive, in seq]

rot_to [lemma, in seq]

rot_to_arc_spec [inductive, in path]

rot_size_cat [lemma, in seq]

rot_add_mod [lemma, in seq]

rot_rot [lemma, in seq]

rot_oversize [lemma, in seq]

rot_rotr [lemma, in seq]

rot_uniq [lemma, in seq]

rot_tupleP [lemma, in tuple]

rot_to_arc [lemma, in path]

rot_addn [lemma, in seq]

rot0 [lemma, in seq]

rot1_cons [lemma, in seq]

row [definition, in matrix]

rowE [lemma, in matrix]

rowg [definition, in mxabelem]

rowgD [lemma, in mxabelem]

rowgI [lemma, in mxabelem]

rowgK [lemma, in mxabelem]

rowgS [lemma, in mxabelem]

rowg_mx1 [lemma, in mxabelem]

rowg_mx_eq0 [lemma, in mxabelem]

rowg_mxS [lemma, in mxabelem]

rowg_stable [lemma, in mxabelem]

rowg_group [definition, in mxabelem]

rowg_mx [definition, in mxabelem]

rowg_mxK [lemma, in mxabelem]

rowg_group_set [lemma, in mxabelem]

rowg_mxSK [lemma, in mxabelem]

rowg0 [lemma, in mxabelem]

rowg1 [lemma, in mxabelem]

rowK [lemma, in matrix]

rowKd [lemma, in matrix]

rowKu [lemma, in matrix]

rowP [lemma, in matrix]

RowPoly [section, in mxpoly]

RowPoly.d [variable, in mxpoly]

RowPoly.R [variable, in mxpoly]

RowSpaceTheory [section, in mxalgebra]

RowSpaceTheory.AddsmxSub [section, in mxalgebra]

RowSpaceTheory.AddsmxSub.A [variable, in mxalgebra]

RowSpaceTheory.AddsmxSub.B [variable, in mxalgebra]

RowSpaceTheory.AddsmxSub.m1 [variable, in mxalgebra]

RowSpaceTheory.AddsmxSub.m2 [variable, in mxalgebra]

RowSpaceTheory.AddsmxSub.n [variable, in mxalgebra]

RowSpaceTheory.BinaryDirect [section, in mxalgebra]

RowSpaceTheory.BinaryDirect.m1 [variable, in mxalgebra]

RowSpaceTheory.BinaryDirect.m2 [variable, in mxalgebra]

RowSpaceTheory.BinaryDirect.n [variable, in mxalgebra]

RowSpaceTheory.Defs [section, in mxalgebra]

RowSpaceTheory.Defs.A [variable, in mxalgebra]

RowSpaceTheory.Defs.m [variable, in mxalgebra]

RowSpaceTheory.Defs.n [variable, in mxalgebra]

RowSpaceTheory.Eigenspace [section, in mxalgebra]

RowSpaceTheory.Eigenspace.g [variable, in mxalgebra]

RowSpaceTheory.Eigenspace.n [variable, in mxalgebra]

RowSpaceTheory.F [variable, in mxalgebra]

RowSpaceTheory.I [variable, in mxalgebra]

RowSpaceTheory.LtmxIdentities [section, in mxalgebra]

RowSpaceTheory.LtmxIdentities.A [variable, in mxalgebra]

RowSpaceTheory.LtmxIdentities.B [variable, in mxalgebra]

RowSpaceTheory.LtmxIdentities.m1 [variable, in mxalgebra]

RowSpaceTheory.LtmxIdentities.m2 [variable, in mxalgebra]

RowSpaceTheory.LtmxIdentities.n [variable, in mxalgebra]

RowSpaceTheory.NaryDirect [section, in mxalgebra]

RowSpaceTheory.NaryDirect.n [variable, in mxalgebra]

RowSpaceTheory.NaryDirect.P [variable, in mxalgebra]

RowSpaceTheory.SubDaddsmx [section, in mxalgebra]

RowSpaceTheory.SubDaddsmx.A [variable, in mxalgebra]

RowSpaceTheory.SubDaddsmx.B1 [variable, in mxalgebra]

RowSpaceTheory.SubDaddsmx.B2 [variable, in mxalgebra]

RowSpaceTheory.SubDaddsmx.m [variable, in mxalgebra]

RowSpaceTheory.SubDaddsmx.m1 [variable, in mxalgebra]

RowSpaceTheory.SubDaddsmx.m2 [variable, in mxalgebra]

RowSpaceTheory.SubDaddsmx.n [variable, in mxalgebra]

RowSpaceTheory.SubDsumsmx [section, in mxalgebra]

RowSpaceTheory.SubDsumsmx.A [variable, in mxalgebra]

RowSpaceTheory.SubDsumsmx.B [variable, in mxalgebra]

RowSpaceTheory.SubDsumsmx.m [variable, in mxalgebra]

RowSpaceTheory.SubDsumsmx.n [variable, in mxalgebra]

RowSpaceTheory.SubDsumsmx.P [variable, in mxalgebra]

RowSpaceTheory.SumExpr [section, in mxalgebra]

RowSpaceTheory.SumExpr.Binary [section, in mxalgebra]

RowSpaceTheory.SumExpr.Binary.m1 [variable, in mxalgebra]

RowSpaceTheory.SumExpr.Binary.m2 [variable, in mxalgebra]

RowSpaceTheory.SumExpr.Binary.n [variable, in mxalgebra]

RowSpaceTheory.SumExpr.Binary.S1 [variable, in mxalgebra]

RowSpaceTheory.SumExpr.Binary.S2 [variable, in mxalgebra]

RowSpaceTheory.SumExpr.Nary [section, in mxalgebra]

RowSpaceTheory.SumExpr.Nary.n [variable, in mxalgebra]

RowSpaceTheory.SumExpr.Nary.P [variable, in mxalgebra]

RowSpaceTheory.SumExpr.Nary.S_ [variable, in mxalgebra]

rowV0P [lemma, in mxalgebra]

rowV0Pn [lemma, in mxalgebra]

row_free_unit [lemma, in mxalgebra]

row_free_map [lemma, in mxalgebra]

row_freeP [lemma, in mxalgebra]

row_full_unit [lemma, in mxalgebra]

row_mx0 [lemma, in matrix]

row_perm_const [lemma, in matrix]

row_full_dom_hom [lemma, in mxrepresentation]

row_subPn [lemma, in mxalgebra]

row_permM [lemma, in matrix]

row_perm1 [lemma, in matrix]

row_full_inj [lemma, in mxalgebra]

row_eq [lemma, in matrix]

row_mxEr [lemma, in matrix]

row_sub [lemma, in mxalgebra]

row_mxEl [lemma, in matrix]

row_row_mx [lemma, in matrix]

row_id [lemma, in matrix]

row_mx_const [lemma, in matrix]

row_subP [lemma, in mxalgebra]

row_free [definition, in mxalgebra]

row_hom_mxP [lemma, in mxrepresentation]

row_permE [lemma, in matrix]

row_leq_rank [lemma, in mxalgebra]

row_mxAx [definition, in matrix]

row_ebase_unit [lemma, in mxalgebra]

row_full_map [lemma, in mxalgebra]

row_perm_linear [definition, in matrix]

row_linear [definition, in matrix]

row_perm_additive [definition, in matrix]

row_additive [definition, in matrix]

row_full [definition, in mxalgebra]

row_base_free [lemma, in mxalgebra]

row_perm [definition, in matrix]

row_base [definition, in mxalgebra]

row_hom_mx [definition, in mxrepresentation]

row_mxA [lemma, in matrix]

row_free_inj [lemma, in mxalgebra]

row_mxKr [lemma, in matrix]

row_mxKl [lemma, in matrix]

row_ebase [definition, in mxalgebra]

row_fullP [lemma, in mxalgebra]

row_mul [lemma, in matrix]

row_sum_delta [lemma, in matrix]

row_const [lemma, in matrix]

row_matrixP [lemma, in matrix]

row_mx [definition, in matrix]

row' [definition, in matrix]

row'Kd [lemma, in matrix]

row'Ku [lemma, in matrix]

row'_const [lemma, in matrix]

row'_row_mx [lemma, in matrix]

row'_linear [definition, in matrix]

row'_additive [definition, in matrix]

row'_eq [lemma, in matrix]

row0 [lemma, in matrix]

row1 [lemma, in matrix]

rrefl [lemma, in ssrfun]

rreg [definition, in poly]

rregM [lemma, in poly]

rregP [lemma, in poly]

rregX [lemma, in poly]

rreg_lead [lemma, in poly]

rreg_size [lemma, in poly]

rreg_div0 [lemma, in poly]

rreg_scale0 [lemma, in poly]

rreg_lead0 [lemma, in poly]

rreg_dvdp_mull [lemma, in poly]

rreg0 [lemma, in poly]

rreg1 [lemma, in poly]

rshift [definition, in fintype]

rshift_subproof [lemma, in fintype]

rshift1 [lemma, in zmodp]

rsimC [abbreviation, in mxrepresentation]

rsimT [abbreviation, in mxrepresentation]

rsim_submod1 [lemma, in mxrepresentation]

rsim_irr_comp [lemma, in mxrepresentation]

rsim_last [definition, in mxrepresentation]

rsim_regular_series [lemma, in mxrepresentation]

rsim_regular_submod [lemma, in mxrepresentation]

rsim_regular_factmod [lemma, in mxrepresentation]

rsim_rcons [definition, in mxrepresentation]

rstab [definition, in mxrepresentation]

rstabS [lemma, in mxrepresentation]

rstabs [definition, in mxrepresentation]

rstabs_morphim [lemma, in mxrepresentation]

rstabs_abelem_rowg_mx [lemma, in mxabelem]

rstabs_abelem [lemma, in mxabelem]

rstabs_group [definition, in mxrepresentation]

rstabs_act [lemma, in mxrepresentation]

rstabs_factmod [lemma, in mxrepresentation]

rstabs_map [lemma, in mxrepresentation]

rstabs_group_set [lemma, in mxrepresentation]

rstabs_eqg [lemma, in mxrepresentation]

rstabs_sub [lemma, in mxrepresentation]

rstabs_conj [lemma, in mxrepresentation]

rstabs_morphpre [lemma, in mxrepresentation]

rstabs_quo [lemma, in mxrepresentation]

rstabs_subg [lemma, in mxrepresentation]

rstabs_submod [lemma, in mxrepresentation]

rstab_factmod [lemma, in mxrepresentation]

rstab_morphpre [lemma, in mxrepresentation]

rstab_eqg [lemma, in mxrepresentation]

rstab_sub [lemma, in mxrepresentation]

rstab_morphim [lemma, in mxrepresentation]

rstab_group [definition, in mxrepresentation]

rstab_conj [lemma, in mxrepresentation]

rstab_subg [lemma, in mxrepresentation]

rstab_map [lemma, in mxrepresentation]

rstab_norm [lemma, in mxrepresentation]

rstab_group_set [lemma, in mxrepresentation]

rstab_submod [lemma, in mxrepresentation]

rstab_abelem [lemma, in mxabelem]

rstab_quo [lemma, in mxrepresentation]

rstab_act [lemma, in mxrepresentation]

rstab_normal [lemma, in mxrepresentation]

rsubmx [definition, in matrix]

rsubmx_linear [definition, in matrix]

rsubmx_additive [definition, in matrix]

rT [abbreviation, in fingroup]

rU [abbreviation, in mxrepresentation]

rU' [abbreviation, in mxrepresentation]

rVabelem [definition, in mxabelem]

rVabelemD [lemma, in mxabelem]

rVabelemJ [lemma, in mxabelem]

rVabelemJmx [definition, in mxabelem]

rVabelemK [lemma, in mxabelem]

rVabelemN [lemma, in mxabelem]

rVabelemS [lemma, in mxabelem]

rVabelemZ [lemma, in mxabelem]

rVabelem_injm [lemma, in mxabelem]

rVabelem_inj [lemma, in mxabelem]

rVabelem_mK [lemma, in mxabelem]

rVabelem_morphism [definition, in mxabelem]

rVabelem_minj [lemma, in mxabelem]

rVabelem0 [lemma, in mxabelem]

rVn [abbreviation, in mxabelem]

rVn [abbreviation, in mxabelem]

rVn [abbreviation, in mxabelem]

rVpoly [definition, in mxpoly]

rVpolyK [lemma, in mxpoly]

rVpoly_delta [lemma, in mxpoly]

rVpoly_linear [definition, in mxpoly]

rVpoly_additive [definition, in mxpoly]

rVpoly_is_linear [lemma, in mxpoly]

rV_eqP [lemma, in mxalgebra]

rV_E [abbreviation, in mxabelem]

rV_abelem_sJ [lemma, in mxabelem]

rV_subP [lemma, in mxalgebra]

rv2v [abbreviation, in vector]

rv2v [abbreviation, in vector]

rv2v [abbreviation, in vector]

rv2v [abbreviation, in vector]

rv2vK [lemma, in vector]

rv2v_linear_proof [lemma, in vector]

rv2v_isomorphism [definition, in vector]

rv2v_proof [lemma, in vector]

rv2v_inj [lemma, in vector]

rv2v_iE [lemma, in vector]

rv2v_bij [lemma, in vector]

rv2v_linear [definition, in vector]

rwP [lemma, in ssrbool]

rwP2 [lemma, in ssrbool]

rZ [definition, in mxabelem]

R_ [abbreviation, in mxrepresentation]

R_G [abbreviation, in mxrepresentation]

r_gt0 [definition, in extremal]

r_gt0 [definition, in extremal]

R_G [abbreviation, in mxrepresentation]

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 | _ | other | (14626 entries) |

Projection 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 | _ | other | (165 entries) |

Record 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 | _ | other | (112 entries) |

Lemma 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 | _ | other | (7292 entries) |

Section 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 | _ | other | (761 entries) |

Constructor 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 | _ | other | (250 entries) |

Abbreviation 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 | _ | other | (390 entries) |

Inductive 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 | _ | other | (84 entries) |

Definition 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 | _ | other | (3144 entries) |

Module 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 | _ | other | (126 entries) |

Axiom 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 | _ | other | (28 entries) |

Variable 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 | _ | other | (2221 entries) |

Library 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 | _ | other | (53 entries) |