| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
F
+F [abbreviation, in mathcomp.field.finfield]+f [abbreviation, in mathcomp.fingroup.gproduct]
+f [abbreviation, in mathcomp.fingroup.automorphism]
+fA [abbreviation, in mathcomp.fingroup.morphism]
+factE [lemma, in mathcomp.ssreflect.ssrnat]
+factm [definition, in mathcomp.fingroup.morphism]
+factmE [lemma, in mathcomp.fingroup.morphism]
+factmod_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
+factmod_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+factmod_mx [definition, in mathcomp.character.mxrepresentation]
+factm_morphM [lemma, in mathcomp.fingroup.morphism]
+factorial [definition, in mathcomp.ssreflect.ssrnat]
+FactorMorphism [section, in mathcomp.fingroup.morphism]
+FactorMorphism.aT [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.f [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.G [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.H [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.q [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.qT [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.rT [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.sGH [variable, in mathcomp.fingroup.morphism]
+FactorMorphism.sKqKf [variable, in mathcomp.fingroup.morphism]
+factor_Xn_sub_1 [lemma, in mathcomp.algebra.poly]
+factor_theorem [lemma, in mathcomp.algebra.poly]
+factS [lemma, in mathcomp.ssreflect.ssrnat]
+fact_prod [lemma, in mathcomp.ssreflect.binomial]
+fact_smonotone [lemma, in mathcomp.ssreflect.binomial]
+fact_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
+fact_rec [definition, in mathcomp.ssreflect.ssrnat]
+fact0 [lemma, in mathcomp.ssreflect.ssrnat]
+FadjoinP [lemma, in mathcomp.field.fieldext]
+Fadjoin_poly_mod [lemma, in mathcomp.field.fieldext]
+Fadjoin_polyX [lemma, in mathcomp.field.fieldext]
+Fadjoin_polyC [lemma, in mathcomp.field.fieldext]
+Fadjoin_poly_unique [lemma, in mathcomp.field.fieldext]
+Fadjoin_polyP [lemma, in mathcomp.field.fieldext]
+Fadjoin_poly_eq [lemma, in mathcomp.field.fieldext]
+Fadjoin_eq_sum [lemma, in mathcomp.field.fieldext]
+Fadjoin_sum_direct [lemma, in mathcomp.field.fieldext]
+Fadjoin_poly_is_linear [lemma, in mathcomp.field.fieldext]
+Fadjoin_polyOver [lemma, in mathcomp.field.fieldext]
+Fadjoin_poly [definition, in mathcomp.field.fieldext]
+Fadjoin_sum [definition, in mathcomp.field.fieldext]
+Fadjoin_seqP [lemma, in mathcomp.field.fieldext]
+Fadjoin_nil [lemma, in mathcomp.field.fieldext]
+Fadjoin_idP [lemma, in mathcomp.field.fieldext]
+Fadjoin0 [lemma, in mathcomp.field.fieldext]
+Fadjoin1_polyP [lemma, in mathcomp.field.fieldext]
+faithful [definition, in mathcomp.fingroup.action]
+faithfulP [lemma, in mathcomp.fingroup.action]
+faithfulR [lemma, in mathcomp.fingroup.action]
+faithful_degree_p_part [lemma, in mathcomp.character.integral_char]
+faithful_isom [lemma, in mathcomp.fingroup.action]
+faithful_repr_extraspecial [lemma, in mathcomp.character.mxabelem]
+Falgebra [module, in mathcomp.field.falgebra]
+falgebra [library]
+FalgebraTheory [section, in mathcomp.field.falgebra]
+FalgebraTheory.aT [variable, in mathcomp.field.falgebra]
+FalgebraTheory.K [variable, in mathcomp.field.falgebra]
+{ aspace _ } (type_scope) [notation, in mathcomp.field.falgebra]
+'Z ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]
+'C ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]
+'C [ _ ] (vspace_scope) [notation, in mathcomp.field.falgebra]
+_ ^+ _ (vspace_scope) [notation, in mathcomp.field.falgebra]
+_ * _ (vspace_scope) [notation, in mathcomp.field.falgebra]
+Falgebra_FieldMixin [lemma, in mathcomp.field.falgebra]
+Falgebra.algType [definition, in mathcomp.field.falgebra]
+Falgebra.BaseMixin [lemma, in mathcomp.field.falgebra]
+Falgebra.BaseType [definition, in mathcomp.field.falgebra]
+Falgebra.base1 [projection, in mathcomp.field.falgebra]
+Falgebra.base2 [definition, in mathcomp.field.falgebra]
+Falgebra.choiceType [definition, in mathcomp.field.falgebra]
+Falgebra.class [definition, in mathcomp.field.falgebra]
+Falgebra.Class [constructor, in mathcomp.field.falgebra]
+Falgebra.ClassDef [section, in mathcomp.field.falgebra]
+Falgebra.ClassDef.cT [variable, in mathcomp.field.falgebra]
+Falgebra.ClassDef.phR [variable, in mathcomp.field.falgebra]
+Falgebra.ClassDef.R [variable, in mathcomp.field.falgebra]
+Falgebra.ClassDef.T [variable, in mathcomp.field.falgebra]
+Falgebra.ClassDef.xT [variable, in mathcomp.field.falgebra]
+Falgebra.class_of [record, in mathcomp.field.falgebra]
+Falgebra.DefaultBase [section, in mathcomp.field.falgebra]
+Falgebra.DefaultBase.A [variable, in mathcomp.field.falgebra]
+Falgebra.DefaultBase.K [variable, in mathcomp.field.falgebra]
+Falgebra.eqType [definition, in mathcomp.field.falgebra]
+Falgebra.Exports [module, in mathcomp.field.falgebra]
+Falgebra.Exports.FalgType [abbreviation, in mathcomp.field.falgebra]
+Falgebra.Exports.FalgUnitRingType [abbreviation, in mathcomp.field.falgebra]
+[ FalgType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.falgebra]
+[ FalgType _ of _ ] (form_scope) [notation, in mathcomp.field.falgebra]
+Falgebra.lalgType [definition, in mathcomp.field.falgebra]
+Falgebra.lmodType [definition, in mathcomp.field.falgebra]
+Falgebra.mixin [projection, in mathcomp.field.falgebra]
+Falgebra.pack [definition, in mathcomp.field.falgebra]
+Falgebra.Pack [constructor, in mathcomp.field.falgebra]
+Falgebra.ringType [definition, in mathcomp.field.falgebra]
+Falgebra.sort [projection, in mathcomp.field.falgebra]
+Falgebra.type [record, in mathcomp.field.falgebra]
+Falgebra.unitAlgType [definition, in mathcomp.field.falgebra]
+Falgebra.unitRingType [definition, in mathcomp.field.falgebra]
+Falgebra.vectType [definition, in mathcomp.field.falgebra]
+Falgebra.vect_unitAlgType [definition, in mathcomp.field.falgebra]
+Falgebra.vect_algType [definition, in mathcomp.field.falgebra]
+Falgebra.vect_lalgType [definition, in mathcomp.field.falgebra]
+Falgebra.vect_unitRingType [definition, in mathcomp.field.falgebra]
+Falgebra.vect_ringType [definition, in mathcomp.field.falgebra]
+Falgebra.xclass [abbreviation, in mathcomp.field.falgebra]
+Falgebra.zmodType [definition, in mathcomp.field.falgebra]
+FalgLfun [module, in mathcomp.field.falgebra]
+FalgLfun.FalgLfun [section, in mathcomp.field.falgebra]
+FalgLfun.FalgLfun.aT [variable, in mathcomp.field.falgebra]
+FalgLfun.FalgLfun.R [variable, in mathcomp.field.falgebra]
+FalgLfun.InvLfun [section, in mathcomp.field.falgebra]
+FalgLfun.InvLfun.aT [variable, in mathcomp.field.falgebra]
+FalgLfun.InvLfun.K [variable, in mathcomp.field.falgebra]
+FalgLfun.lfun_invE [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_unitRingMixin [definition, in mathcomp.field.falgebra]
+FalgLfun.lfun_invr_out [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_unitrP [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_mulrRV [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_mulRVr [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_mulrV [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_mulVr [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_invr [definition, in mathcomp.field.falgebra]
+FalgLfun.lfun_compE [lemma, in mathcomp.field.falgebra]
+FalgLfun.lfun_mulE [lemma, in mathcomp.field.falgebra]
+FalgType_proper [lemma, in mathcomp.field.falgebra]
+falling_factorial [definition, in mathcomp.ssreflect.binomial]
+family [abbreviation, in mathcomp.ssreflect.finfun]
+familyP [lemma, in mathcomp.ssreflect.finfun]
+family_mem [definition, in mathcomp.ssreflect.finfun]
+fcard [abbreviation, in mathcomp.ssreflect.fingraph]
+fcard_id [lemma, in mathcomp.ssreflect.fingraph]
+fcard_order_set [lemma, in mathcomp.ssreflect.fingraph]
+fcard_finv [lemma, in mathcomp.ssreflect.fingraph]
+fcard_mem [abbreviation, in mathcomp.ssreflect.fingraph]
+fclosed [abbreviation, in mathcomp.ssreflect.fingraph]
+fclosed1 [lemma, in mathcomp.ssreflect.fingraph]
+fclosure [abbreviation, in mathcomp.ssreflect.fingraph]
+fconnect [abbreviation, in mathcomp.ssreflect.fingraph]
+FconnectEq [section, in mathcomp.ssreflect.fingraph]
+FconnectEq.eq_rf [variable, in mathcomp.ssreflect.fingraph]
+FconnectEq.eq_f [variable, in mathcomp.ssreflect.fingraph]
+FconnectEq.f [variable, in mathcomp.ssreflect.fingraph]
+FconnectEq.f' [variable, in mathcomp.ssreflect.fingraph]
+FconnectEq.T [variable, in mathcomp.ssreflect.fingraph]
+FconnectId [section, in mathcomp.ssreflect.fingraph]
+FconnectId.T [variable, in mathcomp.ssreflect.fingraph]
+fconnect_id [lemma, in mathcomp.ssreflect.fingraph]
+fconnect_sym [lemma, in mathcomp.ssreflect.fingraph]
+fconnect_sym_in [lemma, in mathcomp.ssreflect.fingraph]
+fconnect_cycle [lemma, in mathcomp.ssreflect.fingraph]
+fconnect_invariant [lemma, in mathcomp.ssreflect.fingraph]
+fconnect_orbit [lemma, in mathcomp.ssreflect.fingraph]
+fconnect_finv [lemma, in mathcomp.ssreflect.fingraph]
+fconnect_iter [lemma, in mathcomp.ssreflect.fingraph]
+fconnect1 [lemma, in mathcomp.ssreflect.fingraph]
+fcycle [abbreviation, in mathcomp.ssreflect.path]
+fE [abbreviation, in mathcomp.fingroup.automorphism]
+Fermat's_little_theorem [lemma, in mathcomp.field.finfield]
+fF [abbreviation, in mathcomp.field.closed_field]
+ff [abbreviation, in mathcomp.fingroup.morphism]
+ffactE [lemma, in mathcomp.ssreflect.binomial]
+ffactnn [lemma, in mathcomp.ssreflect.binomial]
+ffactnS [lemma, in mathcomp.ssreflect.binomial]
+ffactnSr [lemma, in mathcomp.ssreflect.binomial]
+ffactn0 [lemma, in mathcomp.ssreflect.binomial]
+ffactn1 [lemma, in mathcomp.ssreflect.binomial]
+ffactSS [lemma, in mathcomp.ssreflect.binomial]
+ffact_factd [lemma, in mathcomp.ssreflect.binomial]
+ffact_fact [lemma, in mathcomp.ssreflect.binomial]
+ffact_small [lemma, in mathcomp.ssreflect.binomial]
+ffact_gt0 [lemma, in mathcomp.ssreflect.binomial]
+ffact_rec [definition, in mathcomp.ssreflect.binomial]
+ffact0n [lemma, in mathcomp.ssreflect.binomial]
+ffT [abbreviation, in mathcomp.ssreflect.finfun]
+fful_lin_char_inj [lemma, in mathcomp.character.character]
+ffunE [lemma, in mathcomp.ssreflect.finfun]
+ffunK [lemma, in mathcomp.ssreflect.finfun]
+ffunMnE [lemma, in mathcomp.algebra.ssralg]
+ffunMzE [lemma, in mathcomp.algebra.ssrint]
+ffunP [lemma, in mathcomp.ssreflect.finfun]
+ffun_lmodMixin [definition, in mathcomp.algebra.ssralg]
+ffun_scale_addl [lemma, in mathcomp.algebra.ssralg]
+ffun_scale_addr [lemma, in mathcomp.algebra.ssralg]
+ffun_scale1 [lemma, in mathcomp.algebra.ssralg]
+ffun_scaleA [lemma, in mathcomp.algebra.ssralg]
+ffun_scale [definition, in mathcomp.algebra.ssralg]
+ffun_comRingType [definition, in mathcomp.algebra.ssralg]
+ffun_mulC [lemma, in mathcomp.algebra.ssralg]
+ffun_ringType [definition, in mathcomp.algebra.ssralg]
+ffun_ringMixin [definition, in mathcomp.algebra.ssralg]
+ffun_mul_addr [lemma, in mathcomp.algebra.ssralg]
+ffun_mul_addl [lemma, in mathcomp.algebra.ssralg]
+ffun_mul_1r [lemma, in mathcomp.algebra.ssralg]
+ffun_mul_1l [lemma, in mathcomp.algebra.ssralg]
+ffun_mulA [lemma, in mathcomp.algebra.ssralg]
+ffun_mul [definition, in mathcomp.algebra.ssralg]
+ffun_one [definition, in mathcomp.algebra.ssralg]
+ffun_zmodMixin [definition, in mathcomp.algebra.ssralg]
+ffun_addN [lemma, in mathcomp.algebra.ssralg]
+ffun_add0 [lemma, in mathcomp.algebra.ssralg]
+ffun_addC [lemma, in mathcomp.algebra.ssralg]
+ffun_addA [lemma, in mathcomp.algebra.ssralg]
+ffun_add [definition, in mathcomp.algebra.ssralg]
+ffun_opp [definition, in mathcomp.algebra.ssralg]
+ffun_zero [definition, in mathcomp.algebra.ssralg]
+ffun_vectMixin [definition, in mathcomp.algebra.vector]
+ffun_vect_iso [lemma, in mathcomp.algebra.vector]
+ffun_cfInd [definition, in mathcomp.character.classfun]
+ffun_Quo [definition, in mathcomp.character.classfun]
+ffun_on [abbreviation, in mathcomp.ssreflect.finfun]
+ffun_onP [lemma, in mathcomp.ssreflect.finfun]
+ffun_on_mem [definition, in mathcomp.ssreflect.finfun]
+ffun1_nonzero [lemma, in mathcomp.algebra.ssralg]
+fGisom [abbreviation, in mathcomp.fingroup.action]
+fgraph [definition, in mathcomp.ssreflect.finfun]
+fgraph_codom [lemma, in mathcomp.ssreflect.finfun]
+fH [abbreviation, in mathcomp.fingroup.quotient]
+fHisom [abbreviation, in mathcomp.fingroup.action]
+fH_G [abbreviation, in mathcomp.fingroup.quotient]
+Fid [lemma, in mathcomp.solvable.burnside_app]
+Fid3 [lemma, in mathcomp.solvable.burnside_app]
+FieldAutomorphism [section, in mathcomp.character.classfun]
+FieldAutomorphism.f [variable, in mathcomp.character.classfun]
+FieldAutomorphism.G [variable, in mathcomp.character.classfun]
+FieldAutomorphism.gT [variable, in mathcomp.character.classfun]
+FieldAutomorphism.H [variable, in mathcomp.character.classfun]
+FieldAutomorphism.K [variable, in mathcomp.character.classfun]
+FieldAutomorphism.KxH [variable, in mathcomp.character.classfun]
+FieldAutomorphism.R [variable, in mathcomp.character.classfun]
+FieldAutomorphism.rT [variable, in mathcomp.character.classfun]
+FieldAutomorphism.u [variable, in mathcomp.character.classfun]
+_ ^u [notation, in mathcomp.character.classfun]
+FieldExt [module, in mathcomp.field.fieldext]
+fieldext [library]
+FieldExtTheory [section, in mathcomp.field.fieldext]
+FieldExtTheory.FadjoinPoly [section, in mathcomp.field.fieldext]
+FieldExtTheory.FadjoinPolyDefinitions [section, in mathcomp.field.fieldext]
+FieldExtTheory.FadjoinPolyDefinitions.U [variable, in mathcomp.field.fieldext]
+FieldExtTheory.FadjoinPolyDefinitions.x [variable, in mathcomp.field.fieldext]
+FieldExtTheory.FadjoinPoly.K [variable, in mathcomp.field.fieldext]
+FieldExtTheory.FadjoinPoly.nz_x_i [variable, in mathcomp.field.fieldext]
+FieldExtTheory.FadjoinPoly.x [variable, in mathcomp.field.fieldext]
+FieldExtTheory.F0 [variable, in mathcomp.field.fieldext]
+FieldExtTheory.Horner [section, in mathcomp.field.fieldext]
+FieldExtTheory.Horner.z [variable, in mathcomp.field.fieldext]
+FieldExtTheory.L [variable, in mathcomp.field.fieldext]
+fieldExt_hornerZ [lemma, in mathcomp.field.fieldext]
+fieldExt_hornerX [lemma, in mathcomp.field.fieldext]
+fieldExt_hornerC [lemma, in mathcomp.field.fieldext]
+fieldExt_horner [definition, in mathcomp.field.fieldext]
+FieldExt.algType [definition, in mathcomp.field.fieldext]
+FieldExt.alg_fieldType [definition, in mathcomp.field.fieldext]
+FieldExt.alg_idomainType [definition, in mathcomp.field.fieldext]
+FieldExt.alg_comUnitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.alg_comRingType [definition, in mathcomp.field.fieldext]
+FieldExt.base [projection, in mathcomp.field.fieldext]
+FieldExt.base1 [definition, in mathcomp.field.fieldext]
+FieldExt.base2 [definition, in mathcomp.field.fieldext]
+FieldExt.base3 [definition, in mathcomp.field.fieldext]
+FieldExt.base4 [definition, in mathcomp.field.fieldext]
+FieldExt.choiceType [definition, in mathcomp.field.fieldext]
+FieldExt.class [definition, in mathcomp.field.fieldext]
+FieldExt.Class [constructor, in mathcomp.field.fieldext]
+FieldExt.class_of [record, in mathcomp.field.fieldext]
+FieldExt.comm_ext [projection, in mathcomp.field.fieldext]
+FieldExt.comRingType [definition, in mathcomp.field.fieldext]
+FieldExt.comUnitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.eqType [definition, in mathcomp.field.fieldext]
+FieldExt.Exports [module, in mathcomp.field.fieldext]
+FieldExt.Exports.fieldExtType [abbreviation, in mathcomp.field.fieldext]
+[ fieldExtType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.fieldext]
+[ fieldExtType _ of _ ] (form_scope) [notation, in mathcomp.field.fieldext]
+{ subfield _ } (type_scope) [notation, in mathcomp.field.fieldext]
+FieldExt.FalgType [definition, in mathcomp.field.fieldext]
+FieldExt.Falg_fieldType [definition, in mathcomp.field.fieldext]
+FieldExt.Falg_idomainType [definition, in mathcomp.field.fieldext]
+FieldExt.Falg_comUnitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.Falg_comRingType [definition, in mathcomp.field.fieldext]
+FieldExt.FieldExt [section, in mathcomp.field.fieldext]
+FieldExt.FieldExt.Bases [section, in mathcomp.field.fieldext]
+FieldExt.FieldExt.Bases.c [variable, in mathcomp.field.fieldext]
+FieldExt.FieldExt.Bases.T [variable, in mathcomp.field.fieldext]
+FieldExt.FieldExt.cT [variable, in mathcomp.field.fieldext]
+FieldExt.FieldExt.phR [variable, in mathcomp.field.fieldext]
+FieldExt.FieldExt.R [variable, in mathcomp.field.fieldext]
+FieldExt.FieldExt.T [variable, in mathcomp.field.fieldext]
+FieldExt.FieldExt.xT [variable, in mathcomp.field.fieldext]
+FieldExt.fieldType [definition, in mathcomp.field.fieldext]
+FieldExt.field_ext [projection, in mathcomp.field.fieldext]
+FieldExt.idomainType [definition, in mathcomp.field.fieldext]
+FieldExt.idomain_ext [projection, in mathcomp.field.fieldext]
+FieldExt.lalgType [definition, in mathcomp.field.fieldext]
+FieldExt.lalg_fieldType [definition, in mathcomp.field.fieldext]
+FieldExt.lalg_idomainType [definition, in mathcomp.field.fieldext]
+FieldExt.lalg_comUnitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.lalg_comRingType [definition, in mathcomp.field.fieldext]
+FieldExt.lmodType [definition, in mathcomp.field.fieldext]
+FieldExt.lmod_fieldType [definition, in mathcomp.field.fieldext]
+FieldExt.lmod_idomainType [definition, in mathcomp.field.fieldext]
+FieldExt.lmod_comUnitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.lmod_comRingType [definition, in mathcomp.field.fieldext]
+FieldExt.pack [definition, in mathcomp.field.fieldext]
+FieldExt.Pack [constructor, in mathcomp.field.fieldext]
+FieldExt.pack_eta [definition, in mathcomp.field.fieldext]
+FieldExt.ringType [definition, in mathcomp.field.fieldext]
+FieldExt.sort [projection, in mathcomp.field.fieldext]
+FieldExt.type [record, in mathcomp.field.fieldext]
+FieldExt.unitAlgType [definition, in mathcomp.field.fieldext]
+FieldExt.unitAlg_fieldType [definition, in mathcomp.field.fieldext]
+FieldExt.unitAlg_idomainType [definition, in mathcomp.field.fieldext]
+FieldExt.unitAlg_comUnitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.unitAlg_comRingType [definition, in mathcomp.field.fieldext]
+FieldExt.unitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.vectType [definition, in mathcomp.field.fieldext]
+FieldExt.vect_fieldType [definition, in mathcomp.field.fieldext]
+FieldExt.vect_idomainType [definition, in mathcomp.field.fieldext]
+FieldExt.vect_comUnitRingType [definition, in mathcomp.field.fieldext]
+FieldExt.vect_comRingType [definition, in mathcomp.field.fieldext]
+FieldExt.xclass [abbreviation, in mathcomp.field.fieldext]
+FieldExt.zmodType [definition, in mathcomp.field.fieldext]
+FieldMulCyclic [section, in mathcomp.solvable.cyclic]
+FieldMulCyclic.G [variable, in mathcomp.solvable.cyclic]
+FieldMulCyclic.gT [variable, in mathcomp.solvable.cyclic]
+fieldOver [definition, in mathcomp.field.fieldext]
+FieldOver [section, in mathcomp.field.fieldext]
+fieldOver_splitting [lemma, in mathcomp.field.galois]
+fieldOver_vectMixin [lemma, in mathcomp.field.fieldext]
+fieldOver_scaleAr [lemma, in mathcomp.field.fieldext]
+fieldOver_scaleAl [lemma, in mathcomp.field.fieldext]
+fieldOver_scaleE [lemma, in mathcomp.field.fieldext]
+fieldOver_lmodMixin [definition, in mathcomp.field.fieldext]
+fieldOver_scaleDl [lemma, in mathcomp.field.fieldext]
+fieldOver_scaleDr [lemma, in mathcomp.field.fieldext]
+fieldOver_scale1 [lemma, in mathcomp.field.fieldext]
+fieldOver_scaleA [lemma, in mathcomp.field.fieldext]
+fieldOver_scale [definition, in mathcomp.field.fieldext]
+FieldOver.F [variable, in mathcomp.field.fieldext]
+FieldOver.F0 [variable, in mathcomp.field.fieldext]
+FieldOver.L [variable, in mathcomp.field.fieldext]
+_ *F: _ [notation, in mathcomp.field.fieldext]
+FieldRepr [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Abelian [section, in mathcomp.character.mxrepresentation]
+FieldRepr.AbelianQuotient [section, in mathcomp.character.mxrepresentation]
+FieldRepr.AbelianQuotient.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.AbelianQuotient.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.AbelianQuotient.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.AbelianQuotient.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Abelian.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Abelian.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Abelian.splitG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup [section, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.H [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SameGroup [section, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SameGroup.eqGH [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SameGroup.Stabilisers [section, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SameGroup.Stabilisers.m [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SameGroup.Stabilisers.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SubGroup [section, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SubGroup.sHG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SubGroup.Stabilisers [section, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SubGroup.Stabilisers.m [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.ChangeGroup.SubGroup.Stabilisers.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.H [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.irrG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.nHG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.nsHG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.rH [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.sH [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.sHG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Clifford.valWact [variable, in mathcomp.character.mxrepresentation]
+'Cl (action_scope) [notation, in mathcomp.character.mxrepresentation]
+FieldRepr.Conjugate [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Conjugate.B [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Conjugate.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Conjugate.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Conjugate.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Conjugate.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Conjugate.uB [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.F [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JacobsonDensity [section, in mathcomp.character.mxrepresentation]
+FieldRepr.JacobsonDensity.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JacobsonDensity.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JacobsonDensity.irrG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JacobsonDensity.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JacobsonDensity.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder [section, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder.last_mod [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder.rsim_last [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.JordanHolder.rsim_rcons [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.LinearIrr [section, in mathcomp.character.mxrepresentation]
+FieldRepr.LinearIrr.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.LinearIrr.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.aT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.D [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.f [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.rGf [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.rT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.sGD [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.sG_f'fG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.Stabilisers [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.Stabilisers.m [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphim.Stabilisers.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.aT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.D [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.f [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.rT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.Stabilisers [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.Stabilisers.m [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Morphpre.Stabilisers.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.CentHom [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.CentHom.f [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components.defU [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components.iso_u [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components.nz_u [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components.simU [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components.u [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Components.Uu [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Socle [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Socle.sG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Socle.SocleDef [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Socle.SocleDef.sG0 [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Socle.SubSocle [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Socle.SubSocle.P [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Stabilisers [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Stabilisers.m [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Stabilisers.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Submodule [section, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Submodule.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.OneRepresentation.Submodule.Umod [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Proper [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Proper.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Proper.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Proper.n' [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Proper.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.H [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.krH [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.nHG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.nHGs [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Quotient.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.CenterMode [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.CenterMode.i [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.CenterMode.i0 [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.F'G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.GringMx [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.GringMx.F'G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.GringMx.irrG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.GringMx.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.GringMx.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.groupCl [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.IrrComponent [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.IrrComponent.irrG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.IrrComponent.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.IrrComponent.not_rsim_op0 [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.IrrComponent.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.sG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.splitG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Regular.sums_R [variable, in mathcomp.character.mxrepresentation]
+'e_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
+'R_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
+'n_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
+1 (irrType_scope) [notation, in mathcomp.character.mxrepresentation]
+FieldRepr.Similarity [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Similarity.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Similarity.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Socle [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Socle.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Socle.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Socle.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Socle.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Socle.sG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.SplittingField [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Submodule [section, in mathcomp.character.mxrepresentation]
+FieldRepr.Submodule.G [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Submodule.gT [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Submodule.n [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Submodule.rG [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Submodule.U [variable, in mathcomp.character.mxrepresentation]
+FieldRepr.Submodule.Umod [variable, in mathcomp.character.mxrepresentation]
+[ 1 _ ] (irrType_scope) [notation, in mathcomp.character.mxrepresentation]
+FieldRoots [section, in mathcomp.algebra.poly]
+FieldRoots.F [variable, in mathcomp.algebra.poly]
+FieldRoots.UnityRoots [section, in mathcomp.algebra.poly]
+FieldRoots.UnityRoots.n [variable, in mathcomp.algebra.poly]
+FieldRoots.UnityRoots.prim_z [variable, in mathcomp.algebra.poly]
+FieldRoots.UnityRoots.z [variable, in mathcomp.algebra.poly]
+FieldRoots.UnityRoots.zn [variable, in mathcomp.algebra.poly]
+field_module_semisimple [lemma, in mathcomp.field.fieldext]
+field_dimS [lemma, in mathcomp.field.fieldext]
+field_module_dimS [lemma, in mathcomp.field.fieldext]
+field_module_eq [lemma, in mathcomp.field.fieldext]
+field_subvMr [lemma, in mathcomp.field.fieldext]
+field_subvMl [lemma, in mathcomp.field.fieldext]
+field_mem_algid [lemma, in mathcomp.field.fieldext]
+field_unit_group_cyclic [lemma, in mathcomp.solvable.cyclic]
+field_mul_group_cyclic [lemma, in mathcomp.solvable.cyclic]
+filter [definition, in mathcomp.ssreflect.seq]
+FilterSubseq [section, in mathcomp.ssreflect.seq]
+FilterSubseq.T [variable, in mathcomp.ssreflect.seq]
+filter_pi_of [lemma, in mathcomp.ssreflect.prime]
+filter_free [lemma, in mathcomp.algebra.vector]
+filter_flatten [lemma, in mathcomp.ssreflect.seq]
+filter_subseq [lemma, in mathcomp.ssreflect.seq]
+filter_mask [lemma, in mathcomp.ssreflect.seq]
+filter_map [lemma, in mathcomp.ssreflect.seq]
+filter_undup [lemma, in mathcomp.ssreflect.seq]
+filter_pred1_uniq [lemma, in mathcomp.ssreflect.seq]
+filter_uniq [lemma, in mathcomp.ssreflect.seq]
+filter_rev [lemma, in mathcomp.ssreflect.seq]
+filter_predI [lemma, in mathcomp.ssreflect.seq]
+filter_predT [lemma, in mathcomp.ssreflect.seq]
+filter_pred0 [lemma, in mathcomp.ssreflect.seq]
+filter_rcons [lemma, in mathcomp.ssreflect.seq]
+filter_cat [lemma, in mathcomp.ssreflect.seq]
+filter_id [lemma, in mathcomp.ssreflect.seq]
+filter_all [lemma, in mathcomp.ssreflect.seq]
+filter_pairwise_orthogonal [lemma, in mathcomp.character.classfun]
+filter_index_enum [lemma, in mathcomp.ssreflect.bigop]
+FimModAbelem [section, in mathcomp.solvable.abelian]
+finalg [library]
+FinCancel [section, in mathcomp.ssreflect.fintype]
+FinCancel.f [variable, in mathcomp.ssreflect.fintype]
+FinCancel.fK [variable, in mathcomp.ssreflect.fintype]
+FinCancel.g [variable, in mathcomp.ssreflect.fintype]
+FinCancel.Inv [section, in mathcomp.ssreflect.fintype]
+FinCancel.Inv.injf [variable, in mathcomp.ssreflect.fintype]
+FinCancel.T [variable, in mathcomp.ssreflect.fintype]
+finCharP [lemma, in mathcomp.field.finfield]
+find [definition, in mathcomp.ssreflect.seq]
+findex [definition, in mathcomp.ssreflect.fingraph]
+findex_iter [lemma, in mathcomp.ssreflect.fingraph]
+findex_max [lemma, in mathcomp.ssreflect.fingraph]
+findex0 [lemma, in mathcomp.ssreflect.fingraph]
+FinDomain [section, in mathcomp.field.finfield]
+FinDomainFieldType [definition, in mathcomp.field.finfield]
+FinDomainSplittingFieldType [definition, in mathcomp.field.finfield]
+finDomain_mulrC [lemma, in mathcomp.field.finfield]
+finDomain_field [lemma, in mathcomp.field.finfield]
+FinDomain.domR [variable, in mathcomp.field.finfield]
+FinDomain.lregR [variable, in mathcomp.field.finfield]
+FinDomain.R [variable, in mathcomp.field.finfield]
+_ %| _ [notation, in mathcomp.field.finfield]
+find_map [lemma, in mathcomp.ssreflect.seq]
+find_nseq [lemma, in mathcomp.ssreflect.seq]
+find_cat [lemma, in mathcomp.ssreflect.seq]
+find_size [lemma, in mathcomp.ssreflect.seq]
+find_ex_minn [lemma, in mathcomp.ssreflect.ssrnat]
+FinField [section, in mathcomp.field.finfield]
+finfield [library]
+FinFieldExists [section, in mathcomp.field.finfield]
+FinFieldExists.map_poly_extField [variable, in mathcomp.field.finfield]
+_ ^%:A (ring_scope) [notation, in mathcomp.field.finfield]
+FinFieldExtType [abbreviation, in mathcomp.field.finfield]
+FinFieldRepr [section, in mathcomp.character.mxabelem]
+FinFieldRepr.F [variable, in mathcomp.character.mxabelem]
+FinFieldRepr.G [variable, in mathcomp.character.mxabelem]
+FinFieldRepr.gT [variable, in mathcomp.character.mxabelem]
+FinFieldRepr.n' [variable, in mathcomp.character.mxabelem]
+FinFieldRepr.rG [variable, in mathcomp.character.mxabelem]
+FinFieldRepr.RowGroup [section, in mathcomp.character.mxabelem]
+FinFieldRepr.RowGroup.n [variable, in mathcomp.character.mxabelem]
+FinFieldRepr.ScaleAction [section, in mathcomp.character.mxabelem]
+FinFieldRepr.ScaleAction.m [variable, in mathcomp.character.mxabelem]
+FinFieldRepr.ScaleAction.n [variable, in mathcomp.character.mxabelem]
+'Zm (action_scope) [notation, in mathcomp.character.mxabelem]
+finField_galois_generator [lemma, in mathcomp.field.finfield]
+finField_galois [lemma, in mathcomp.field.finfield]
+finField_is_abelem [lemma, in mathcomp.field.finfield]
+finField_genPoly [lemma, in mathcomp.field.finfield]
+finField_unit [definition, in mathcomp.field.finfield]
+FinField.F [variable, in mathcomp.field.finfield]
+finfun [abbreviation, in mathcomp.ssreflect.finfun]
+Finfun [constructor, in mathcomp.ssreflect.finfun]
+finfun [library]
+FinFunComRing [section, in mathcomp.algebra.ssralg]
+FinFunComRing.a [variable, in mathcomp.algebra.ssralg]
+FinFunComRing.aT [variable, in mathcomp.algebra.ssralg]
+FinFunComRing.R [variable, in mathcomp.algebra.ssralg]
+FinFunLmod [section, in mathcomp.algebra.ssralg]
+FinFunLmod.aT [variable, in mathcomp.algebra.ssralg]
+FinFunLmod.R [variable, in mathcomp.algebra.ssralg]
+FinFunLmod.rT [variable, in mathcomp.algebra.ssralg]
+FinFunRing [section, in mathcomp.algebra.ssralg]
+FinFunRing.a [variable, in mathcomp.algebra.ssralg]
+FinFunRing.aT [variable, in mathcomp.algebra.ssralg]
+FinFunRing.R [variable, in mathcomp.algebra.ssralg]
+FinFunZmod [section, in mathcomp.algebra.ssralg]
+FinFunZmod.aT [variable, in mathcomp.algebra.ssralg]
+FinFunZmod.rT [variable, in mathcomp.algebra.ssralg]
+FinFunZmod.Sum [section, in mathcomp.algebra.ssralg]
+FinFunZmod.Sum.F [variable, in mathcomp.algebra.ssralg]
+FinFunZmod.Sum.I [variable, in mathcomp.algebra.ssralg]
+FinFunZmod.Sum.P [variable, in mathcomp.algebra.ssralg]
+FinFunZmod.Sum.r [variable, in mathcomp.algebra.ssralg]
+finfun_finMixin [definition, in mathcomp.ssreflect.finfun]
+finfun_countMixin [definition, in mathcomp.ssreflect.finfun]
+finfun_choiceMixin [definition, in mathcomp.ssreflect.finfun]
+finfun_eqMixin [definition, in mathcomp.ssreflect.finfun]
+finfun_def [abbreviation, in mathcomp.ssreflect.finfun]
+finfun_of [definition, in mathcomp.ssreflect.finfun]
+finfun_type [inductive, in mathcomp.ssreflect.finfun]
+finfun_of_set [definition, in mathcomp.ssreflect.finset]
+fingraph [library]
+FinGroup [module, in mathcomp.fingroup.fingroup]
+fingroup [library]
+FinGroup.arg_finType [definition, in mathcomp.fingroup.fingroup]
+FinGroup.arg_countType [definition, in mathcomp.fingroup.fingroup]
+FinGroup.arg_choiceType [definition, in mathcomp.fingroup.fingroup]
+FinGroup.arg_eqType [definition, in mathcomp.fingroup.fingroup]
+FinGroup.arg_sort [definition, in mathcomp.fingroup.fingroup]
+FinGroup.base [projection, in mathcomp.fingroup.fingroup]
+FinGroup.BaseMixin [constructor, in mathcomp.fingroup.fingroup]
+FinGroup.base_type [record, in mathcomp.fingroup.fingroup]
+FinGroup.class [abbreviation, in mathcomp.fingroup.fingroup]
+FinGroup.clone [definition, in mathcomp.fingroup.fingroup]
+FinGroup.clone_base [definition, in mathcomp.fingroup.fingroup]
+FinGroup.Exports [module, in mathcomp.fingroup.fingroup]
+FinGroup.Exports.BaseFinGroupType [abbreviation, in mathcomp.fingroup.fingroup]
+FinGroup.Exports.baseFinGroupType [abbreviation, in mathcomp.fingroup.fingroup]
+FinGroup.Exports.FinGroupType [abbreviation, in mathcomp.fingroup.fingroup]
+FinGroup.Exports.finGroupType [abbreviation, in mathcomp.fingroup.fingroup]
+[ finGroupType of _ ] (form_scope) [notation, in mathcomp.fingroup.fingroup]
+[ baseFinGroupType of _ ] (form_scope) [notation, in mathcomp.fingroup.fingroup]
+FinGroup.finClass [definition, in mathcomp.fingroup.fingroup]
+FinGroup.InheritedClasses [section, in mathcomp.fingroup.fingroup]
+FinGroup.InheritedClasses.bT [variable, in mathcomp.fingroup.fingroup]
+FinGroup.inv [projection, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin [definition, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin [section, in mathcomp.fingroup.fingroup]
+FinGroup.mixin [definition, in mathcomp.fingroup.fingroup]
+FinGroup.mixin_of [record, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin.inv [variable, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin.mul [variable, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin.mulA [variable, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin.mulV [variable, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin.mul1 [variable, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin.one [variable, in mathcomp.fingroup.fingroup]
+FinGroup.Mixin.T [variable, in mathcomp.fingroup.fingroup]
+_ ^-1 [notation, in mathcomp.fingroup.fingroup]
+_ * _ [notation, in mathcomp.fingroup.fingroup]
+1 [notation, in mathcomp.fingroup.fingroup]
+FinGroup.mk_invMg [lemma, in mathcomp.fingroup.fingroup]
+FinGroup.mk_invgK [lemma, in mathcomp.fingroup.fingroup]
+FinGroup.mul [projection, in mathcomp.fingroup.fingroup]
+FinGroup.one [projection, in mathcomp.fingroup.fingroup]
+FinGroup.Pack [constructor, in mathcomp.fingroup.fingroup]
+FinGroup.PackBase [constructor, in mathcomp.fingroup.fingroup]
+FinGroup.pack_base [definition, in mathcomp.fingroup.fingroup]
+FinGroup.rT [abbreviation, in mathcomp.fingroup.fingroup]
+FinGroup.sort [projection, in mathcomp.fingroup.fingroup]
+FinGroup.T [abbreviation, in mathcomp.fingroup.fingroup]
+FinGroup.type [record, in mathcomp.fingroup.fingroup]
+Finite [module, in mathcomp.ssreflect.fintype]
+FiniteModule [module, in mathcomp.solvable.finmodule]
+FiniteModule.actAr [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actNr [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actr [definition, in mathcomp.solvable.finmodule]
+FiniteModule.actrK [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actrKV [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actrM [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actr_is_groupAction [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actr_sum [definition, in mathcomp.solvable.finmodule]
+FiniteModule.actr_is_action [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actr1 [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.actZr [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.act0r [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.congr_fmod [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmod [definition, in mathcomp.solvable.finmodule]
+FiniteModule.Fmod [constructor, in mathcomp.solvable.finmodule]
+FiniteModule.fmodA [abbreviation, in mathcomp.solvable.finmodule]
+FiniteModule.fmodJ [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmodK [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmodKcond [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmodM [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmodP [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmodV [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmodX [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_inj [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_zmodMixin [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_addrC [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_addNr [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_addrA [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_add0r [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_add [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_opp [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_finMixin [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_countMixin [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_choiceMixin [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_eqMixin [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmod_of [inductive, in mathcomp.solvable.finmodule]
+FiniteModule.fmod1 [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmval [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmvalA [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmvalJ [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmvalJcond [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmvalK [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmvalN [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmvalZ [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.fmval_sum [definition, in mathcomp.solvable.finmodule]
+FiniteModule.fmval0 [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.injm_fmod [lemma, in mathcomp.solvable.finmodule]
+FiniteModule.OneFinMod [section, in mathcomp.solvable.finmodule]
+FiniteModule.OneFinMod.A [variable, in mathcomp.solvable.finmodule]
+FiniteModule.OneFinMod.abelA [variable, in mathcomp.solvable.finmodule]
+FiniteModule.OneFinMod.f2sub [variable, in mathcomp.solvable.finmodule]
+FiniteModule.OneFinMod.gT [variable, in mathcomp.solvable.finmodule]
+FiniteModule.OneFinMod.sub2f [variable, in mathcomp.solvable.finmodule]
+'M (action_scope) [notation, in mathcomp.solvable.finmodule]
+'M (groupAction_scope) [notation, in mathcomp.solvable.finmodule]
+_ ^@ _ (ring_scope) [notation, in mathcomp.solvable.finmodule]
+FiniteModule.valA [abbreviation, in mathcomp.solvable.finmodule]
+'M (action_scope) [notation, in mathcomp.solvable.finmodule]
+'M (groupAction_scope) [notation, in mathcomp.solvable.finmodule]
+_ ^@ _ (ring_scope) [notation, in mathcomp.solvable.finmodule]
+FiniteQuant [module, in mathcomp.ssreflect.fintype]
+FiniteQuant.all [definition, in mathcomp.ssreflect.fintype]
+FiniteQuant.all_in [definition, in mathcomp.ssreflect.fintype]
+FiniteQuant.Definitions [section, in mathcomp.ssreflect.fintype]
+FiniteQuant.Definitions.T [variable, in mathcomp.ssreflect.fintype]
+FiniteQuant.ex [definition, in mathcomp.ssreflect.fintype]
+FiniteQuant.Exports [module, in mathcomp.ssreflect.fintype]
+, exists _ : _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ : _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists ( _ : _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists ( _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ : _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ : _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ : _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall ( _ : _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall ( _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ : _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists ( _ : _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists ( _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists _ : _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall ( _ : _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall ( _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ : _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+FiniteQuant.ex_in [definition, in mathcomp.ssreflect.fintype]
+FiniteQuant.Quantified [constructor, in mathcomp.ssreflect.fintype]
+FiniteQuant.quantified [inductive, in mathcomp.ssreflect.fintype]
+FiniteQuant.quant0b [definition, in mathcomp.ssreflect.fintype]
+_ ^~ [notation, in mathcomp.ssreflect.fintype]
+_ ^* [notation, in mathcomp.ssreflect.fintype]
+[ _ : _ | _ ] [notation, in mathcomp.ssreflect.fintype]
+[ _ | _ ] [notation, in mathcomp.ssreflect.fintype]
+finite_PET [lemma, in mathcomp.field.separable]
+Finite.axiom [definition, in mathcomp.ssreflect.fintype]
+Finite.base [projection, in mathcomp.ssreflect.fintype]
+Finite.base2 [definition, in mathcomp.ssreflect.fintype]
+Finite.choiceType [definition, in mathcomp.ssreflect.fintype]
+Finite.class [definition, in mathcomp.ssreflect.fintype]
+Finite.Class [constructor, in mathcomp.ssreflect.fintype]
+Finite.ClassDef [section, in mathcomp.ssreflect.fintype]
+Finite.ClassDef.cT [variable, in mathcomp.ssreflect.fintype]
+Finite.ClassDef.T [variable, in mathcomp.ssreflect.fintype]
+Finite.ClassDef.xT [variable, in mathcomp.ssreflect.fintype]
+Finite.class_of [record, in mathcomp.ssreflect.fintype]
+Finite.clone [definition, in mathcomp.ssreflect.fintype]
+Finite.CountMixin [definition, in mathcomp.ssreflect.fintype]
+Finite.countType [definition, in mathcomp.ssreflect.fintype]
+Finite.count_enumP [lemma, in mathcomp.ssreflect.fintype]
+Finite.count_enum [definition, in mathcomp.ssreflect.fintype]
+Finite.enum [abbreviation, in mathcomp.ssreflect.fintype]
+Finite.EnumDef [module, in mathcomp.ssreflect.fintype]
+Finite.EnumDef.enum [definition, in mathcomp.ssreflect.fintype]
+Finite.EnumDef.enumDef [definition, in mathcomp.ssreflect.fintype]
+Finite.EnumMixin [definition, in mathcomp.ssreflect.fintype]
+Finite.EnumSig [module, in mathcomp.ssreflect.fintype]
+Finite.EnumSig.enum [axiom, in mathcomp.ssreflect.fintype]
+Finite.EnumSig.enumDef [axiom, in mathcomp.ssreflect.fintype]
+Finite.eqType [definition, in mathcomp.ssreflect.fintype]
+Finite.Exports [module, in mathcomp.ssreflect.fintype]
+Finite.Exports.FinMixin [abbreviation, in mathcomp.ssreflect.fintype]
+Finite.Exports.FinType [abbreviation, in mathcomp.ssreflect.fintype]
+Finite.Exports.finType [abbreviation, in mathcomp.ssreflect.fintype]
+Finite.Exports.UniqFinMixin [abbreviation, in mathcomp.ssreflect.fintype]
+[ finType of _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
+[ finType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
+Finite.mixin [projection, in mathcomp.ssreflect.fintype]
+Finite.Mixin [constructor, in mathcomp.ssreflect.fintype]
+Finite.Mixins [section, in mathcomp.ssreflect.fintype]
+Finite.Mixins.n [variable, in mathcomp.ssreflect.fintype]
+Finite.Mixins.T [variable, in mathcomp.ssreflect.fintype]
+Finite.Mixins.ubT [variable, in mathcomp.ssreflect.fintype]
+Finite.mixin_enum [projection, in mathcomp.ssreflect.fintype]
+Finite.mixin_base [projection, in mathcomp.ssreflect.fintype]
+Finite.mixin_of [record, in mathcomp.ssreflect.fintype]
+Finite.pack [definition, in mathcomp.ssreflect.fintype]
+Finite.Pack [constructor, in mathcomp.ssreflect.fintype]
+Finite.RawMixin [section, in mathcomp.ssreflect.fintype]
+Finite.RawMixin.T [variable, in mathcomp.ssreflect.fintype]
+Finite.sort [projection, in mathcomp.ssreflect.fintype]
+Finite.type [record, in mathcomp.ssreflect.fintype]
+Finite.UniqMixin [definition, in mathcomp.ssreflect.fintype]
+Finite.uniq_enumP [lemma, in mathcomp.ssreflect.fintype]
+Finite.xclass [abbreviation, in mathcomp.ssreflect.fintype]
+finmodule [library]
+FinRing [section, in mathcomp.field.finfield]
+FinRing [module, in mathcomp.algebra.finalg]
+FinRingRepr [section, in mathcomp.character.mxabelem]
+FinRingRepr.G [variable, in mathcomp.character.mxabelem]
+FinRingRepr.gT [variable, in mathcomp.character.mxabelem]
+FinRingRepr.n [variable, in mathcomp.character.mxabelem]
+FinRingRepr.R [variable, in mathcomp.character.mxabelem]
+FinRingRepr.rG [variable, in mathcomp.character.mxabelem]
+finRing_gt1 [lemma, in mathcomp.field.finfield]
+finRing_nontrivial [lemma, in mathcomp.field.finfield]
+FinRing.AdditiveGroup [section, in mathcomp.algebra.finalg]
+FinRing.AdditiveGroup.U [variable, in mathcomp.algebra.finalg]
+FinRing.Algebra [module, in mathcomp.algebra.finalg]
+FinRing.Algebra.algType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.base [projection, in mathcomp.algebra.finalg]
+FinRing.Algebra.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.class [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.Algebra.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.Algebra.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.Algebra.ClassDef.phR [variable, in mathcomp.algebra.finalg]
+FinRing.Algebra.ClassDef.R [variable, in mathcomp.algebra.finalg]
+FinRing.Algebra.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.Algebra.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Algebra.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.Exports [module, in mathcomp.algebra.finalg]
+FinRing.Algebra.Exports.finAlgType [abbreviation, in mathcomp.algebra.finalg]
+[ finAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.Algebra.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.finType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.join_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.join_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.lalgType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.lmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.Algebra.pack [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.Algebra.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.sort [projection, in mathcomp.algebra.finalg]
+FinRing.Algebra.type [record, in mathcomp.algebra.finalg]
+FinRing.Algebra.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Algebra.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.base_group [abbreviation, in mathcomp.algebra.finalg]
+FinRing.ComRing [module, in mathcomp.algebra.finalg]
+FinRing.ComRing.base [projection, in mathcomp.algebra.finalg]
+FinRing.ComRing.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.class [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.ComRing.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.ComRing.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.ComRing.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.ComRing.class_of [record, in mathcomp.algebra.finalg]
+FinRing.ComRing.comRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.Exports [module, in mathcomp.algebra.finalg]
+FinRing.ComRing.Exports.finComRingType [abbreviation, in mathcomp.algebra.finalg]
+[ finComRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.ComRing.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.ComRing.pack [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.ComRing.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.sort [projection, in mathcomp.algebra.finalg]
+FinRing.ComRing.type [record, in mathcomp.algebra.finalg]
+FinRing.ComRing.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.ComRing.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing [module, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.base [projection, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.base3 [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.cjoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.class [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.class_of [record, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.Exports [module, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.Exports.finComUnitRingType [abbreviation, in mathcomp.algebra.finalg]
+[ finComUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.fcjoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.join_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.pack [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.sort [projection, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.type [record, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.ujoin_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField [module, in mathcomp.algebra.finalg]
+FinRing.DecField.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.Exports [module, in mathcomp.algebra.finalg]
+FinRing.DecField.finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.finIdomainType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.finType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.DecField.Joins [section, in mathcomp.algebra.finalg]
+FinRing.DecField.Joins.cT [variable, in mathcomp.algebra.finalg]
+FinRing.DecField.Joins.xclass [variable, in mathcomp.algebra.finalg]
+FinRing.DecField.Joins.xT [variable, in mathcomp.algebra.finalg]
+FinRing.DecField.type [definition, in mathcomp.algebra.finalg]
+FinRing.decidable [lemma, in mathcomp.algebra.finalg]
+FinRing.DecidableFieldMixin [definition, in mathcomp.algebra.finalg]
+FinRing.DecideField [section, in mathcomp.algebra.finalg]
+FinRing.DecideField.F [variable, in mathcomp.algebra.finalg]
+FinRing.do_pack [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Field [module, in mathcomp.algebra.finalg]
+FinRing.Field.base [projection, in mathcomp.algebra.finalg]
+FinRing.Field.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.Field.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.class [definition, in mathcomp.algebra.finalg]
+FinRing.Field.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.Field.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.Field.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.Field.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.Field.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Field.comRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.comUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.Exports [module, in mathcomp.algebra.finalg]
+FinRing.Field.Exports.finFieldType [abbreviation, in mathcomp.algebra.finalg]
+[ finFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.Field.fieldType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finIdomainType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.idomainType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finIdomainType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.Field.pack [definition, in mathcomp.algebra.finalg]
+FinRing.Field.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.Field.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.sort [projection, in mathcomp.algebra.finalg]
+FinRing.Field.type [record, in mathcomp.algebra.finalg]
+FinRing.Field.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Field.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.fin_group [abbreviation, in mathcomp.algebra.finalg]
+FinRing.fin_ [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Generic [section, in mathcomp.algebra.finalg]
+FinRing.Generic.base_class [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.base_sort [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.base_of [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.base_type [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.Class [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.class_of [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.Pack [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.to_choice [variable, in mathcomp.algebra.finalg]
+FinRing.Generic.type [variable, in mathcomp.algebra.finalg]
+FinRing.gen_pack [definition, in mathcomp.algebra.finalg]
+FinRing.groupMixin [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain [module, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.base [projection, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.class [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.class_of [record, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.comRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.comUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.Exports [module, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.Exports.finIdomainType [abbreviation, in mathcomp.algebra.finalg]
+[ finIdomainType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.finType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomainType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.pack [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.sort [projection, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.type [record, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra [module, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.base [projection, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.base3 [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.class [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.ClassDef.phR [variable, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.ClassDef.R [variable, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.Exports [module, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.Exports.finLalgType [abbreviation, in mathcomp.algebra.finalg]
+[ finLalgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.fljoin_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.join_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalgType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.ljoin_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.pack [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.rjoin_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.sort [projection, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.type [record, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule [module, in mathcomp.algebra.finalg]
+FinRing.Lmodule.base [projection, in mathcomp.algebra.finalg]
+FinRing.Lmodule.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.class [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.Lmodule.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.Lmodule.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.Lmodule.ClassDef.phR [variable, in mathcomp.algebra.finalg]
+FinRing.Lmodule.ClassDef.R [variable, in mathcomp.algebra.finalg]
+FinRing.Lmodule.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.Lmodule.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Lmodule.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.Exports [module, in mathcomp.algebra.finalg]
+FinRing.Lmodule.Exports.finLmodType [abbreviation, in mathcomp.algebra.finalg]
+[ finLmodType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.Lmodule.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.finType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.Lmodule.pack [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.Lmodule.sort [projection, in mathcomp.algebra.finalg]
+FinRing.Lmodule.type [record, in mathcomp.algebra.finalg]
+FinRing.Lmodule.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Lmodule.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.mixin_of [abbreviation, in mathcomp.algebra.finalg]
+FinRing.R [variable, in mathcomp.field.finfield]
+FinRing.Ring [module, in mathcomp.algebra.finalg]
+FinRing.Ring.base [projection, in mathcomp.algebra.finalg]
+FinRing.Ring.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.class [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.Ring.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.Ring.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.Ring.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.Ring.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Ring.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.Exports [module, in mathcomp.algebra.finalg]
+FinRing.Ring.Exports.finRingType [abbreviation, in mathcomp.algebra.finalg]
+[ finRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.Ring.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.finType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.intro_unit [lemma, in mathcomp.algebra.finalg]
+FinRing.Ring.inv [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.invr_out [lemma, in mathcomp.algebra.finalg]
+FinRing.Ring.is_inv [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.Ring.mulrV [lemma, in mathcomp.algebra.finalg]
+FinRing.Ring.mulVr [lemma, in mathcomp.algebra.finalg]
+FinRing.Ring.pack [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.Ring.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.sort [projection, in mathcomp.algebra.finalg]
+FinRing.Ring.type [record, in mathcomp.algebra.finalg]
+FinRing.Ring.unit [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.Unit [section, in mathcomp.algebra.finalg]
+FinRing.Ring.UnitMixin [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.Unit.R [variable, in mathcomp.algebra.finalg]
+FinRing.Ring.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Ring.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.sat [definition, in mathcomp.algebra.finalg]
+FinRing.Theory [module, in mathcomp.algebra.finalg]
+FinRing.Theory.unit_actE [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.val_unitV [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.val_unitX [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.val_unitM [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.val_unit1 [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.zmodMgE [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.zmodVgE [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.zmodXgE [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.zmod_abelian [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.zmod_mulgC [definition, in mathcomp.algebra.finalg]
+FinRing.Theory.zmod1gE [definition, in mathcomp.algebra.finalg]
+FinRing.unit [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Unit [constructor, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra [module, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ajoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.algType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.base [projection, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.base3 [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.class [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ClassDef.phR [variable, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ClassDef.R [variable, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.class_of [record, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.Exports [module, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.Exports.finUnitAlgType [abbreviation, in mathcomp.algebra.finalg]
+[ finUnitAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.fajoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.fljoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.fnjoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.lalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ljoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.lmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.njoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.pack [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.sort [projection, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.type [record, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ujoin_finAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ujoin_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.ujoin_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing [module, in mathcomp.algebra.finalg]
+FinRing.UnitRing.base [projection, in mathcomp.algebra.finalg]
+FinRing.UnitRing.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.base2 [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.class [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.UnitRing.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.UnitRing.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.UnitRing.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.UnitRing.class_of [record, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.Exports [module, in mathcomp.algebra.finalg]
+FinRing.UnitRing.Exports.finUnitRingType [abbreviation, in mathcomp.algebra.finalg]
+[ finUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.UnitRing.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.finType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.join_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.join_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.UnitRing.pack [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.UnitRing.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.sort [projection, in mathcomp.algebra.finalg]
+FinRing.UnitRing.type [record, in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.UnitRing.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitsGroup [section, in mathcomp.algebra.finalg]
+FinRing.UnitsGroupExports [module, in mathcomp.algebra.finalg]
+FinRing.UnitsGroup.phR [variable, in mathcomp.algebra.finalg]
+FinRing.UnitsGroup.R [variable, in mathcomp.algebra.finalg]
+FinRing.unit_is_groupAction [lemma, in mathcomp.algebra.finalg]
+FinRing.unit_actE [lemma, in mathcomp.algebra.finalg]
+FinRing.unit_act [definition, in mathcomp.algebra.finalg]
+FinRing.unit_GroupMixin [definition, in mathcomp.algebra.finalg]
+FinRing.unit_mulVu [lemma, in mathcomp.algebra.finalg]
+FinRing.unit_mul1u [lemma, in mathcomp.algebra.finalg]
+FinRing.unit_muluA [lemma, in mathcomp.algebra.finalg]
+FinRing.unit_mul [definition, in mathcomp.algebra.finalg]
+FinRing.unit_mul_proof [lemma, in mathcomp.algebra.finalg]
+FinRing.unit_inv [definition, in mathcomp.algebra.finalg]
+FinRing.unit_inv_proof [lemma, in mathcomp.algebra.finalg]
+FinRing.unit_finMixin [definition, in mathcomp.algebra.finalg]
+FinRing.unit_countMixin [definition, in mathcomp.algebra.finalg]
+FinRing.unit_choiceMixin [definition, in mathcomp.algebra.finalg]
+FinRing.unit_eqMixin [definition, in mathcomp.algebra.finalg]
+FinRing.unit_of [inductive, in mathcomp.algebra.finalg]
+FinRing.unit1 [definition, in mathcomp.algebra.finalg]
+FinRing.uT [abbreviation, in mathcomp.algebra.finalg]
+FinRing.uval [definition, in mathcomp.algebra.finalg]
+FinRing.val_unitX [lemma, in mathcomp.algebra.finalg]
+FinRing.val_unitV [lemma, in mathcomp.algebra.finalg]
+FinRing.val_unitM [lemma, in mathcomp.algebra.finalg]
+FinRing.val_unit1 [lemma, in mathcomp.algebra.finalg]
+FinRing.zmodMgE [lemma, in mathcomp.algebra.finalg]
+FinRing.Zmodule [module, in mathcomp.algebra.finalg]
+FinRing.Zmodule.base [projection, in mathcomp.algebra.finalg]
+FinRing.Zmodule.baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.choiceType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.class [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.Class [constructor, in mathcomp.algebra.finalg]
+FinRing.Zmodule.ClassDef [section, in mathcomp.algebra.finalg]
+FinRing.Zmodule.ClassDef.cT [variable, in mathcomp.algebra.finalg]
+FinRing.Zmodule.ClassDef.xT [variable, in mathcomp.algebra.finalg]
+FinRing.Zmodule.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Zmodule.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.eqType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.Exports [module, in mathcomp.algebra.finalg]
+FinRing.Zmodule.Exports.finZmodType [abbreviation, in mathcomp.algebra.finalg]
+[ finGroupType of _ for +%R ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ baseFinGroupType of _ for +%R ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finZmodType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+FinRing.Zmodule.finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.finType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.join_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.mixin [projection, in mathcomp.algebra.finalg]
+FinRing.Zmodule.pack [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.Pack [constructor, in mathcomp.algebra.finalg]
+FinRing.Zmodule.sort [projection, in mathcomp.algebra.finalg]
+FinRing.Zmodule.type [record, in mathcomp.algebra.finalg]
+FinRing.Zmodule.xclass [abbreviation, in mathcomp.algebra.finalg]
+FinRing.Zmodule.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.zmodVgE [lemma, in mathcomp.algebra.finalg]
+FinRing.zmodXgE [lemma, in mathcomp.algebra.finalg]
+FinRing.zmod_abelian [lemma, in mathcomp.algebra.finalg]
+FinRing.zmod_mulgC [lemma, in mathcomp.algebra.finalg]
+FinRing.zmod1gE [lemma, in mathcomp.algebra.finalg]
+finset [abbreviation, in mathcomp.ssreflect.finset]
+FinSet [constructor, in mathcomp.ssreflect.finset]
+finset [library]
+finset_def [abbreviation, in mathcomp.ssreflect.finset]
+FinSplittingField [section, in mathcomp.field.finfield]
+FinSplittingFieldAxiom [abbreviation, in mathcomp.field.finfield]
+FinSplittingFieldFor [lemma, in mathcomp.field.finfield]
+FinSplittingFieldType [abbreviation, in mathcomp.field.finfield]
+FinSplittingField.F [variable, in mathcomp.field.finfield]
+FinSplittingField.FinGalois [section, in mathcomp.field.finfield]
+FinSplittingField.FinGalois.galL [variable, in mathcomp.field.finfield]
+FinSplittingField.FinGalois.L [variable, in mathcomp.field.finfield]
+FinSplittingField.order [variable, in mathcomp.field.finfield]
+FinTheory [section, in mathcomp.ssreflect.finfun]
+FinTheory.aT [variable, in mathcomp.ssreflect.finfun]
+FinTheory.rT [variable, in mathcomp.ssreflect.finfun]
+FinTuple [module, in mathcomp.ssreflect.tuple]
+FinTupleSig [module, in mathcomp.ssreflect.tuple]
+FinTupleSig.enum [axiom, in mathcomp.ssreflect.tuple]
+FinTupleSig.enumP [axiom, in mathcomp.ssreflect.tuple]
+FinTupleSig.FinTupleSig [section, in mathcomp.ssreflect.tuple]
+FinTupleSig.FinTupleSig.n [variable, in mathcomp.ssreflect.tuple]
+FinTupleSig.FinTupleSig.T [variable, in mathcomp.ssreflect.tuple]
+FinTupleSig.size_enum [axiom, in mathcomp.ssreflect.tuple]
+FinTuple.enum [definition, in mathcomp.ssreflect.tuple]
+FinTuple.enumP [lemma, in mathcomp.ssreflect.tuple]
+FinTuple.FinTuple [section, in mathcomp.ssreflect.tuple]
+FinTuple.FinTuple.n [variable, in mathcomp.ssreflect.tuple]
+FinTuple.FinTuple.T [variable, in mathcomp.ssreflect.tuple]
+FinTuple.size_enum [lemma, in mathcomp.ssreflect.tuple]
+fintype [library]
+FinTypeForSub [section, in mathcomp.ssreflect.fintype]
+FinTypeForSub.P [variable, in mathcomp.ssreflect.fintype]
+FinTypeForSub.sfT [variable, in mathcomp.ssreflect.fintype]
+FinTypeForSub.sT [variable, in mathcomp.ssreflect.fintype]
+FinTypeForSub.T [variable, in mathcomp.ssreflect.fintype]
+FinUnitMatrix [section, in mathcomp.algebra.matrix]
+FinUnitMatrix.n [variable, in mathcomp.algebra.matrix]
+FinUnitMatrix.R [variable, in mathcomp.algebra.matrix]
+finv [definition, in mathcomp.ssreflect.fingraph]
+FinVector [module, in mathcomp.field.finfield]
+FinVector.finField_splittingField_axiom [lemma, in mathcomp.field.finfield]
+FinVector.Interfaces [section, in mathcomp.field.finfield]
+FinVector.Interfaces.F [variable, in mathcomp.field.finfield]
+FinvEq [section, in mathcomp.ssreflect.fingraph]
+FinvEq.f [variable, in mathcomp.ssreflect.fingraph]
+FinvEq.injf [variable, in mathcomp.ssreflect.fingraph]
+FinvEq.T [variable, in mathcomp.ssreflect.fingraph]
+finv_inv [lemma, in mathcomp.ssreflect.fingraph]
+finv_eq_can [lemma, in mathcomp.ssreflect.fingraph]
+finv_inj [lemma, in mathcomp.ssreflect.fingraph]
+finv_bij [lemma, in mathcomp.ssreflect.fingraph]
+finv_f [lemma, in mathcomp.ssreflect.fingraph]
+finv_inj_in [lemma, in mathcomp.ssreflect.fingraph]
+finv_f_in [lemma, in mathcomp.ssreflect.fingraph]
+finv_in [lemma, in mathcomp.ssreflect.fingraph]
+FinZmodMatrix [section, in mathcomp.algebra.matrix]
+FinZmodMatrix.m [variable, in mathcomp.algebra.matrix]
+FinZmodMatrix.n [variable, in mathcomp.algebra.matrix]
+FinZmodMatrix.V [variable, in mathcomp.algebra.matrix]
+fin_Csubring_Aint [lemma, in mathcomp.field.algnum]
+fin_ring_char_abelem [lemma, in mathcomp.solvable.abelian]
+fin_Fp_lmod_abelem [lemma, in mathcomp.solvable.abelian]
+fin_lmod_char_abelem [lemma, in mathcomp.solvable.abelian]
+fin_all_exists2 [lemma, in mathcomp.ssreflect.fintype]
+fin_all_exists [lemma, in mathcomp.ssreflect.fintype]
+fin_pred_sort [definition, in mathcomp.ssreflect.fintype]
+fin_inj_bij [lemma, in mathcomp.ssreflect.fingraph]
+FirstIsomorphism [section, in mathcomp.fingroup.quotient]
+FirstIsomorphism.aT [variable, in mathcomp.fingroup.quotient]
+FirstIsomorphism.f [variable, in mathcomp.fingroup.quotient]
+FirstIsomorphism.G [variable, in mathcomp.fingroup.quotient]
+FirstIsomorphism.H [variable, in mathcomp.fingroup.quotient]
+FirstIsomorphism.rT [variable, in mathcomp.fingroup.quotient]
+FirstIsomorphism.sHG [variable, in mathcomp.fingroup.quotient]
+first_isog_loc [lemma, in mathcomp.fingroup.quotient]
+first_isom_loc [lemma, in mathcomp.fingroup.quotient]
+first_isog [lemma, in mathcomp.fingroup.quotient]
+first_isom [lemma, in mathcomp.fingroup.quotient]
+first_orthogonality_relation [lemma, in mathcomp.character.character]
+Fitting [section, in mathcomp.solvable.maximal]
+Fitting [definition, in mathcomp.solvable.maximal]
+FittingEgen [lemma, in mathcomp.solvable.maximal]
+FittingFun [section, in mathcomp.solvable.maximal]
+FittingJ [lemma, in mathcomp.solvable.maximal]
+FittingS [lemma, in mathcomp.solvable.maximal]
+Fitting_pcore [lemma, in mathcomp.solvable.maximal]
+Fitting_char [lemma, in mathcomp.solvable.maximal]
+Fitting_eq_pcore [lemma, in mathcomp.solvable.maximal]
+Fitting_max [lemma, in mathcomp.solvable.maximal]
+Fitting_nil [lemma, in mathcomp.solvable.maximal]
+Fitting_sub [lemma, in mathcomp.solvable.maximal]
+Fitting_normal [lemma, in mathcomp.solvable.maximal]
+Fitting_group_set [lemma, in mathcomp.solvable.maximal]
+Fitting.gT [variable, in mathcomp.solvable.maximal]
+fixedField [definition, in mathcomp.field.galois]
+fixedFieldP [lemma, in mathcomp.field.galois]
+fixedFieldS [lemma, in mathcomp.field.galois]
+fixedField_galois [lemma, in mathcomp.field.galois]
+fixedField_bound [lemma, in mathcomp.field.galois]
+fixedField_is_aspace [lemma, in mathcomp.field.galois]
+fixedPoly_gal [lemma, in mathcomp.field.galois]
+fixedSpace [definition, in mathcomp.algebra.vector]
+FixedSpace [section, in mathcomp.algebra.vector]
+fixedSpaceP [lemma, in mathcomp.algebra.vector]
+fixedSpacesP [lemma, in mathcomp.algebra.vector]
+fixedSpace_id [lemma, in mathcomp.algebra.vector]
+fixedSpace_limg [lemma, in mathcomp.algebra.vector]
+FixedSpace.K [variable, in mathcomp.algebra.vector]
+FixedSpace.vT [variable, in mathcomp.algebra.vector]
+fixed_gal [lemma, in mathcomp.field.galois]
+flatmx0 [lemma, in mathcomp.algebra.matrix]
+flatten [definition, in mathcomp.ssreflect.seq]
+Flatten [section, in mathcomp.ssreflect.seq]
+flattenK [lemma, in mathcomp.ssreflect.seq]
+flattenP [lemma, in mathcomp.ssreflect.seq]
+flatten_mapP [lemma, in mathcomp.ssreflect.seq]
+flatten_indexKr [lemma, in mathcomp.ssreflect.seq]
+flatten_indexKl [lemma, in mathcomp.ssreflect.seq]
+flatten_indexP [lemma, in mathcomp.ssreflect.seq]
+flatten_seq1 [lemma, in mathcomp.ssreflect.seq]
+flatten_rcons [lemma, in mathcomp.ssreflect.seq]
+flatten_cat [lemma, in mathcomp.ssreflect.seq]
+flatten_index [definition, in mathcomp.ssreflect.seq]
+flatten_imageP [lemma, in mathcomp.ssreflect.fintype]
+Flatten.T [variable, in mathcomp.ssreflect.seq]
+floorCD [lemma, in mathcomp.field.algC]
+floorCK [lemma, in mathcomp.field.algC]
+floorCM [lemma, in mathcomp.field.algC]
+floorCN [lemma, in mathcomp.field.algC]
+floorCpK [lemma, in mathcomp.field.algC]
+floorCpP [lemma, in mathcomp.field.algC]
+floorCX [lemma, in mathcomp.field.algC]
+floorC_def [lemma, in mathcomp.field.algC]
+floorC_itv [lemma, in mathcomp.field.algC]
+floorC0 [lemma, in mathcomp.field.algC]
+floorC1 [lemma, in mathcomp.field.algC]
+fmem [definition, in mathcomp.ssreflect.finfun]
+fmod [abbreviation, in mathcomp.solvable.finmodule]
+Fmorph [section, in mathcomp.algebra.rat]
+fmorphXz [lemma, in mathcomp.algebra.ssrint]
+fmorph_eq_rat [lemma, in mathcomp.algebra.rat]
+fmorph_rat [lemma, in mathcomp.algebra.rat]
+fmorph_numZ [lemma, in mathcomp.field.algnum]
+fmorph_primitive_root [lemma, in mathcomp.algebra.poly]
+fmorph_unity_root [lemma, in mathcomp.algebra.poly]
+fmorph_root [lemma, in mathcomp.algebra.poly]
+foldl [definition, in mathcomp.ssreflect.seq]
+FoldLeft [section, in mathcomp.ssreflect.seq]
+FoldLeft.f [variable, in mathcomp.ssreflect.seq]
+FoldLeft.R [variable, in mathcomp.ssreflect.seq]
+FoldLeft.T [variable, in mathcomp.ssreflect.seq]
+foldl_cat [lemma, in mathcomp.ssreflect.seq]
+foldl_rev [lemma, in mathcomp.ssreflect.seq]
+foldr [definition, in mathcomp.ssreflect.seq]
+FoldRight [section, in mathcomp.ssreflect.seq]
+FoldRightComp [section, in mathcomp.ssreflect.seq]
+FoldRightComp.f [variable, in mathcomp.ssreflect.seq]
+FoldRightComp.h [variable, in mathcomp.ssreflect.seq]
+FoldRightComp.R [variable, in mathcomp.ssreflect.seq]
+FoldRightComp.T1 [variable, in mathcomp.ssreflect.seq]
+FoldRightComp.T2 [variable, in mathcomp.ssreflect.seq]
+FoldRightComp.z0 [variable, in mathcomp.ssreflect.seq]
+FoldRight.f [variable, in mathcomp.ssreflect.seq]
+FoldRight.R [variable, in mathcomp.ssreflect.seq]
+FoldRight.T [variable, in mathcomp.ssreflect.seq]
+FoldRight.z0 [variable, in mathcomp.ssreflect.seq]
+foldr_map [lemma, in mathcomp.ssreflect.seq]
+foldr_cat [lemma, in mathcomp.ssreflect.seq]
+forallb_tnth [lemma, in mathcomp.ssreflect.tuple]
+forallP [lemma, in mathcomp.ssreflect.fintype]
+forallPP [lemma, in mathcomp.ssreflect.fintype]
+forall_inP [lemma, in mathcomp.ssreflect.fintype]
+fp [abbreviation, in mathcomp.algebra.mxpoly]
+fp [abbreviation, in mathcomp.algebra.mxpoly]
+fp [abbreviation, in mathcomp.algebra.mxpoly]
+fpath [abbreviation, in mathcomp.ssreflect.path]
+fpathP [lemma, in mathcomp.ssreflect.path]
+fpath_traject [lemma, in mathcomp.ssreflect.path]
+fpath_finv [lemma, in mathcomp.ssreflect.fingraph]
+fpath_f_finv_in [lemma, in mathcomp.ssreflect.fingraph]
+fpath_finv_f_in [lemma, in mathcomp.ssreflect.fingraph]
+fpath_finv_in [lemma, in mathcomp.ssreflect.fingraph]
+Fp_idomainMixin [definition, in mathcomp.algebra.zmodp]
+Fp_fieldMixin [lemma, in mathcomp.algebra.zmodp]
+Fp_nat_mod [lemma, in mathcomp.algebra.zmodp]
+Fp_cast [lemma, in mathcomp.algebra.zmodp]
+Fp_Zcast [lemma, in mathcomp.algebra.zmodp]
+frac [projection, in mathcomp.algebra.fraction]
+FracDomain [section, in mathcomp.algebra.fraction]
+FracDomain.R [variable, in mathcomp.algebra.fraction]
+{ ratio _ } [notation, in mathcomp.algebra.fraction]
+FracField [module, in mathcomp.algebra.fraction]
+FracFieldTheory [section, in mathcomp.algebra.fraction]
+FracFieldTheory.R [variable, in mathcomp.algebra.fraction]
+_ %:F [notation, in mathcomp.algebra.fraction]
+FracField.add [definition, in mathcomp.algebra.fraction]
+FracField.addA [lemma, in mathcomp.algebra.fraction]
+FracField.addC [lemma, in mathcomp.algebra.fraction]
+FracField.addf [definition, in mathcomp.algebra.fraction]
+FracField.addN_l [lemma, in mathcomp.algebra.fraction]
+FracField.add0_l [lemma, in mathcomp.algebra.fraction]
+FracField.dom [abbreviation, in mathcomp.algebra.fraction]
+FracField.domP [abbreviation, in mathcomp.algebra.fraction]
+FracField.equivf [definition, in mathcomp.algebra.fraction]
+FracField.equivfE [lemma, in mathcomp.algebra.fraction]
+FracField.equivf_l [lemma, in mathcomp.algebra.fraction]
+FracField.equivf_r [lemma, in mathcomp.algebra.fraction]
+FracField.equivf_def [lemma, in mathcomp.algebra.fraction]
+FracField.equivf_trans [lemma, in mathcomp.algebra.fraction]
+FracField.equivf_sym [lemma, in mathcomp.algebra.fraction]
+FracField.equivf_refl [lemma, in mathcomp.algebra.fraction]
+FracField.equivf_notation [abbreviation, in mathcomp.algebra.fraction]
+FracField.field_axiom [lemma, in mathcomp.algebra.fraction]
+FracField.frac [abbreviation, in mathcomp.algebra.fraction]
+FracField.FracField [section, in mathcomp.algebra.fraction]
+FracField.FracField.R [variable, in mathcomp.algebra.fraction]
+_ %:F [notation, in mathcomp.algebra.fraction]
+{ fraction _ } [notation, in mathcomp.algebra.fraction]
+FracField.frac_comRingMixin [definition, in mathcomp.algebra.fraction]
+FracField.frac_zmodMixin [definition, in mathcomp.algebra.fraction]
+FracField.inv [definition, in mathcomp.algebra.fraction]
+FracField.invf [definition, in mathcomp.algebra.fraction]
+FracField.inv0 [lemma, in mathcomp.algebra.fraction]
+FracField.mul [definition, in mathcomp.algebra.fraction]
+FracField.mulA [lemma, in mathcomp.algebra.fraction]
+FracField.mulC [lemma, in mathcomp.algebra.fraction]
+FracField.mulf [definition, in mathcomp.algebra.fraction]
+FracField.mulV_l [lemma, in mathcomp.algebra.fraction]
+FracField.mul_addl [lemma, in mathcomp.algebra.fraction]
+FracField.mul1_l [lemma, in mathcomp.algebra.fraction]
+FracField.nonzero1 [lemma, in mathcomp.algebra.fraction]
+FracField.numer0 [lemma, in mathcomp.algebra.fraction]
+FracField.opp [definition, in mathcomp.algebra.fraction]
+FracField.oppf [definition, in mathcomp.algebra.fraction]
+FracField.pi_inv [lemma, in mathcomp.algebra.fraction]
+FracField.pi_mul [lemma, in mathcomp.algebra.fraction]
+FracField.pi_opp [lemma, in mathcomp.algebra.fraction]
+FracField.pi_add [lemma, in mathcomp.algebra.fraction]
+FracField.RatFieldIdomainMixin [definition, in mathcomp.algebra.fraction]
+FracField.RatFieldUnitMixin [definition, in mathcomp.algebra.fraction]
+FracField.Ratio_numden [lemma, in mathcomp.algebra.fraction]
+FracField.tofrac [definition, in mathcomp.algebra.fraction]
+FracField.type [definition, in mathcomp.algebra.fraction]
+FracField.type_of [definition, in mathcomp.algebra.fraction]
+fracq [definition, in mathcomp.algebra.rat]
+fracqE [lemma, in mathcomp.algebra.rat]
+fracqMM [lemma, in mathcomp.algebra.rat]
+fracqP [lemma, in mathcomp.algebra.rat]
+FracqSpecN [constructor, in mathcomp.algebra.rat]
+FracqSpecP [constructor, in mathcomp.algebra.rat]
+fracq_eq0 [lemma, in mathcomp.algebra.rat]
+fracq_eq [lemma, in mathcomp.algebra.rat]
+fracq_spec [inductive, in mathcomp.algebra.rat]
+fracq_subproof [lemma, in mathcomp.algebra.rat]
+fracq0 [lemma, in mathcomp.algebra.rat]
+fraction [library]
+frac0q [lemma, in mathcomp.algebra.rat]
+Frattini [section, in mathcomp.solvable.maximal]
+Frattini [definition, in mathcomp.solvable.maximal]
+Frattini_continuous [lemma, in mathcomp.solvable.maximal]
+Frattini_arg [lemma, in mathcomp.solvable.sylow]
+Frattini.gT [variable, in mathcomp.solvable.maximal]
+Frattini0 [section, in mathcomp.solvable.maximal]
+Frattini0.gT [variable, in mathcomp.solvable.maximal]
+Frattini2 [section, in mathcomp.solvable.maximal]
+Frattini2.gT [variable, in mathcomp.solvable.maximal]
+Frattini2.P [variable, in mathcomp.solvable.maximal]
+Frattini2.p [variable, in mathcomp.solvable.maximal]
+Frattini3 [section, in mathcomp.solvable.maximal]
+Frattini3.gT [variable, in mathcomp.solvable.maximal]
+Frattini3.P [variable, in mathcomp.solvable.maximal]
+Frattini3.p [variable, in mathcomp.solvable.maximal]
+Frattini3.pP [variable, in mathcomp.solvable.maximal]
+Frattini4 [section, in mathcomp.solvable.maximal]
+Frattini4.gT [variable, in mathcomp.solvable.maximal]
+Frattini4.p [variable, in mathcomp.solvable.maximal]
+free [definition, in mathcomp.algebra.vector]
+freeE [lemma, in mathcomp.algebra.vector]
+freeNE [lemma, in mathcomp.algebra.vector]
+freeP [lemma, in mathcomp.algebra.vector]
+free_span [lemma, in mathcomp.algebra.vector]
+free_uniq [lemma, in mathcomp.algebra.vector]
+free_cons [lemma, in mathcomp.algebra.vector]
+free_not0 [lemma, in mathcomp.algebra.vector]
+free_directv [lemma, in mathcomp.algebra.vector]
+frel [definition, in mathcomp.ssreflect.eqtype]
+Frobenius [section, in mathcomp.character.inertia]
+frobenius [library]
+FrobeniusBasics [section, in mathcomp.solvable.frobenius]
+FrobeniusBasics.FrobeniusProperties [section, in mathcomp.solvable.frobenius]
+FrobeniusBasics.FrobeniusProperties.frobG [variable, in mathcomp.solvable.frobenius]
+FrobeniusBasics.FrobeniusProperties.G [variable, in mathcomp.solvable.frobenius]
+FrobeniusBasics.FrobeniusProperties.H [variable, in mathcomp.solvable.frobenius]
+FrobeniusBasics.FrobeniusProperties.K [variable, in mathcomp.solvable.frobenius]
+FrobeniusBasics.gT [variable, in mathcomp.solvable.frobenius]
+FrobeniusJ [lemma, in mathcomp.solvable.frobenius]
+FrobeniusJcompl [lemma, in mathcomp.solvable.frobenius]
+FrobeniusJgroup [lemma, in mathcomp.solvable.frobenius]
+FrobeniusJker [lemma, in mathcomp.solvable.frobenius]
+FrobeniusW [lemma, in mathcomp.solvable.frobenius]
+FrobeniusWcompl [lemma, in mathcomp.solvable.frobenius]
+FrobeniusWker [lemma, in mathcomp.solvable.frobenius]
+Frobenius_Ldiv [lemma, in mathcomp.solvable.frobenius]
+Frobenius_coprime_quotient [lemma, in mathcomp.solvable.frobenius]
+Frobenius_action_kernel_def [lemma, in mathcomp.solvable.frobenius]
+Frobenius_kerS [lemma, in mathcomp.solvable.frobenius]
+Frobenius_kerP [lemma, in mathcomp.solvable.frobenius]
+Frobenius_subr [lemma, in mathcomp.solvable.frobenius]
+Frobenius_subl [lemma, in mathcomp.solvable.frobenius]
+Frobenius_semiregularP [lemma, in mathcomp.solvable.frobenius]
+Frobenius_ker_coprime [lemma, in mathcomp.solvable.frobenius]
+Frobenius_ker_dvd_ker1 [lemma, in mathcomp.solvable.frobenius]
+Frobenius_compl_Hall [lemma, in mathcomp.solvable.frobenius]
+Frobenius_ker_Hall [lemma, in mathcomp.solvable.frobenius]
+Frobenius_index_coprime [lemma, in mathcomp.solvable.frobenius]
+Frobenius_trivg_cent [lemma, in mathcomp.solvable.frobenius]
+Frobenius_coprime [lemma, in mathcomp.solvable.frobenius]
+Frobenius_index_dvd_ker1 [lemma, in mathcomp.solvable.frobenius]
+Frobenius_dvd_ker1 [lemma, in mathcomp.solvable.frobenius]
+Frobenius_reg_compl [lemma, in mathcomp.solvable.frobenius]
+Frobenius_reg_ker [lemma, in mathcomp.solvable.frobenius]
+Frobenius_cent1_ker [lemma, in mathcomp.solvable.frobenius]
+Frobenius_partition [lemma, in mathcomp.solvable.frobenius]
+Frobenius_context [lemma, in mathcomp.solvable.frobenius]
+Frobenius_actionP [lemma, in mathcomp.solvable.frobenius]
+Frobenius_action [definition, in mathcomp.solvable.frobenius]
+Frobenius_group_with_kernel [definition, in mathcomp.solvable.frobenius]
+Frobenius_group_with_kernel_and_complement [definition, in mathcomp.solvable.frobenius]
+Frobenius_group [definition, in mathcomp.solvable.frobenius]
+Frobenius_group_with_complement [definition, in mathcomp.solvable.frobenius]
+Frobenius_kernel_exists [lemma, in mathcomp.character.vcharacter]
+Frobenius_aut [abbreviation, in mathcomp.algebra.ssralg]
+Frobenius_Ind_irrP [lemma, in mathcomp.character.inertia]
+Frobenius_Cauchy [lemma, in mathcomp.fingroup.action]
+Frobenius_reciprocity [lemma, in mathcomp.character.classfun]
+Frobenius_aut_int [lemma, in mathcomp.algebra.ssrint]
+Frobenius_autMz [lemma, in mathcomp.algebra.ssrint]
+Frobenius.frobGK [variable, in mathcomp.character.inertia]
+Frobenius.G [variable, in mathcomp.character.inertia]
+Frobenius.gT [variable, in mathcomp.character.inertia]
+Frobenius.K [variable, in mathcomp.character.inertia]
+froot [abbreviation, in mathcomp.ssreflect.fingraph]
+froots [abbreviation, in mathcomp.ssreflect.fingraph]
+froots_id [lemma, in mathcomp.ssreflect.fingraph]
+froot_id [lemma, in mathcomp.ssreflect.fingraph]
+fsH [abbreviation, in mathcomp.fingroup.gproduct]
+fsK [abbreviation, in mathcomp.fingroup.gproduct]
+fst_morphM [lemma, in mathcomp.fingroup.gproduct]
+fT [abbreviation, in mathcomp.ssreflect.finfun]
+fT [abbreviation, in mathcomp.ssreflect.finfun]
+fT [abbreviation, in mathcomp.ssreflect.finfun]
+fullv [definition, in mathcomp.algebra.vector]
+FunctorGroup [section, in mathcomp.solvable.gfunctor]
+FunctorGroup.F [variable, in mathcomp.solvable.gfunctor]
+FunctorGroup.G [variable, in mathcomp.solvable.gfunctor]
+FunctorGroup.gT [variable, in mathcomp.solvable.gfunctor]
+Functors [section, in mathcomp.solvable.abelian]
+Functors.A [variable, in mathcomp.solvable.abelian]
+Functors.gT [variable, in mathcomp.solvable.abelian]
+Functors.n [variable, in mathcomp.solvable.abelian]
+FunctorTheory [section, in mathcomp.solvable.gfunctor]
+FunctorTheory.F [variable, in mathcomp.solvable.gfunctor]
+Fundamental_Theorem_of_Algebraics [lemma, in mathcomp.field.algebraics_fundamentals]
+FunDelta [constructor, in mathcomp.ssreflect.eqtype]
+FunFinfun [module, in mathcomp.ssreflect.finfun]
+FunFinfunSig [module, in mathcomp.ssreflect.finfun]
+FunFinfunSig.finfun [axiom, in mathcomp.ssreflect.finfun]
+FunFinfunSig.finfunE [axiom, in mathcomp.ssreflect.finfun]
+FunFinfunSig.fun_of_finE [axiom, in mathcomp.ssreflect.finfun]
+FunFinfunSig.fun_of_fin [axiom, in mathcomp.ssreflect.finfun]
+FunFinfun.finfun [definition, in mathcomp.ssreflect.finfun]
+FunFinfun.finfunE [lemma, in mathcomp.ssreflect.finfun]
+FunFinfun.fun_of_finE [lemma, in mathcomp.ssreflect.finfun]
+FunFinfun.fun_of_fin [definition, in mathcomp.ssreflect.finfun]
+FunImage [section, in mathcomp.ssreflect.finset]
+FunImageComp [section, in mathcomp.ssreflect.finset]
+FunImageComp.T [variable, in mathcomp.ssreflect.finset]
+FunImageComp.T' [variable, in mathcomp.ssreflect.finset]
+FunImageComp.U [variable, in mathcomp.ssreflect.finset]
+FunImage.aT [variable, in mathcomp.ssreflect.finset]
+FunImage.aT2 [variable, in mathcomp.ssreflect.finset]
+FunImage.ImsetTheory [section, in mathcomp.ssreflect.finset]
+FunImage.ImsetTheory.ImsetProp [section, in mathcomp.ssreflect.finset]
+FunImage.ImsetTheory.ImsetProp.f [variable, in mathcomp.ssreflect.finset]
+FunImage.ImsetTheory.ImsetProp.f2 [variable, in mathcomp.ssreflect.finset]
+FunImage.ImsetTheory.rT [variable, in mathcomp.ssreflect.finset]
+FunVectType [section, in mathcomp.algebra.vector]
+FunVectType.I [variable, in mathcomp.algebra.vector]
+FunVectType.R [variable, in mathcomp.algebra.vector]
+FunVectType.vT [variable, in mathcomp.algebra.vector]
+FunWith [section, in mathcomp.ssreflect.eqtype]
+FunWith.aT [variable, in mathcomp.ssreflect.eqtype]
+FunWith.rT [variable, in mathcomp.ssreflect.eqtype]
+fun_base [definition, in mathcomp.ssreflect.path]
+fun_of_perm [abbreviation, in mathcomp.fingroup.perm]
+fun_of_perm_def [abbreviation, in mathcomp.fingroup.perm]
+fun_of_lfunK [lemma, in mathcomp.algebra.vector]
+fun_of_lfun [definition, in mathcomp.algebra.vector]
+fun_of_lfun_def [definition, in mathcomp.algebra.vector]
+fun_of_matrix [definition, in mathcomp.algebra.matrix]
+fun_of_cfun [definition, in mathcomp.character.classfun]
+fun_of_fin [abbreviation, in mathcomp.ssreflect.finfun]
+fun_of_fin_def [abbreviation, in mathcomp.ssreflect.finfun]
+fun_delta [inductive, in mathcomp.ssreflect.eqtype]
+fun_adjunction [abbreviation, in mathcomp.ssreflect.fingraph]
+Fun2Set1 [section, in mathcomp.ssreflect.finset]
+Fun2Set1.aT1 [variable, in mathcomp.ssreflect.finset]
+Fun2Set1.aT2 [variable, in mathcomp.ssreflect.finset]
+Fun2Set1.f [variable, in mathcomp.ssreflect.finset]
+Fun2Set1.rT [variable, in mathcomp.ssreflect.finset]
+fwith [definition, in mathcomp.ssreflect.eqtype]
+f_invF [lemma, in mathcomp.ssreflect.fintype]
+f_iinv [lemma, in mathcomp.ssreflect.fintype]
+f_finv [lemma, in mathcomp.ssreflect.fingraph]
+f_finv_in [lemma, in mathcomp.ssreflect.fingraph]
+F_s6 [lemma, in mathcomp.solvable.burnside_app]
+F_s5 [lemma, in mathcomp.solvable.burnside_app]
+F_s4 [lemma, in mathcomp.solvable.burnside_app]
+F_s3 [lemma, in mathcomp.solvable.burnside_app]
+F_s2 [lemma, in mathcomp.solvable.burnside_app]
+F_s1 [lemma, in mathcomp.solvable.burnside_app]
+F_r034 [lemma, in mathcomp.solvable.burnside_app]
+F_r043 [lemma, in mathcomp.solvable.burnside_app]
+F_r013 [lemma, in mathcomp.solvable.burnside_app]
+F_r031 [lemma, in mathcomp.solvable.burnside_app]
+F_r021 [lemma, in mathcomp.solvable.burnside_app]
+F_r012 [lemma, in mathcomp.solvable.burnside_app]
+F_r042 [lemma, in mathcomp.solvable.burnside_app]
+F_r024 [lemma, in mathcomp.solvable.burnside_app]
+F_r41 [lemma, in mathcomp.solvable.burnside_app]
+F_r14 [lemma, in mathcomp.solvable.burnside_app]
+F_r32 [lemma, in mathcomp.solvable.burnside_app]
+F_r23 [lemma, in mathcomp.solvable.burnside_app]
+F_r50 [lemma, in mathcomp.solvable.burnside_app]
+F_r05 [lemma, in mathcomp.solvable.burnside_app]
+F_s23 [lemma, in mathcomp.solvable.burnside_app]
+F_s14 [lemma, in mathcomp.solvable.burnside_app]
+F_s05 [lemma, in mathcomp.solvable.burnside_app]
+F_Sd2 [lemma, in mathcomp.solvable.burnside_app]
+F_Sd1 [lemma, in mathcomp.solvable.burnside_app]
+F_r3 [lemma, in mathcomp.solvable.burnside_app]
+F_r1 [lemma, in mathcomp.solvable.burnside_app]
+F_r2 [lemma, in mathcomp.solvable.burnside_app]
+F_Sv [lemma, in mathcomp.solvable.burnside_app]
+F_Sh [lemma, in mathcomp.solvable.burnside_app]
+F0 [definition, in mathcomp.solvable.burnside_app]
+F1 [abbreviation, in mathcomp.field.fieldext]
+F1 [definition, in mathcomp.solvable.burnside_app]
+F2 [definition, in mathcomp.solvable.burnside_app]
+F3 [definition, in mathcomp.solvable.burnside_app]
+F4 [definition, in mathcomp.solvable.burnside_app]
+F5 [definition, in mathcomp.solvable.burnside_app]
+
| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +