| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 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.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]
-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]
-ffun0 [lemma, in mathcomp.ssreflect.finfun]
-ffun1_nonzero [lemma, in mathcomp.algebra.ssralg]
-fGisom [abbreviation, in mathcomp.fingroup.action]
-fgraph [definition, in mathcomp.ssreflect.finfun]
-fgraphK [lemma, in mathcomp.ssreflect.finfun]
-fgraph_codom [lemma, in mathcomp.ssreflect.finfun]
-fgraph_ffun0 [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_nseq [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]
-FinDepTheory [section, in mathcomp.ssreflect.finfun]
-FinDepTheory.aT [variable, in mathcomp.ssreflect.finfun]
-FinDepTheory.rT [variable, in mathcomp.ssreflect.finfun]
-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 [definition, in mathcomp.ssreflect.finfun]
-finfun [abbreviation, 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]
-FinfunDef [module, in mathcomp.ssreflect.finfun]
-FinfunDefSig [module, in mathcomp.ssreflect.finfun]
-FinfunDefSig.finfun [axiom, in mathcomp.ssreflect.finfun]
-FinfunDefSig.finfunE [axiom, in mathcomp.ssreflect.finfun]
-FinfunDef.finfun [definition, in mathcomp.ssreflect.finfun]
-FinfunDef.finfunE [lemma, in mathcomp.ssreflect.finfun]
-FinfunK [lemma, in mathcomp.ssreflect.finfun]
-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]
-FinfunOf [constructor, in mathcomp.ssreflect.finfun]
-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]
-FinFunTheory [section, in mathcomp.ssreflect.finfun]
-FinFunTheory.aT [variable, in mathcomp.ssreflect.finfun]
-FinFunTheory.rT [variable, in mathcomp.ssreflect.finfun]
-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_def [abbreviation, in mathcomp.ssreflect.finfun]
-finfun_of [inductive, in mathcomp.ssreflect.finfun]
-finfun_rec [definition, in mathcomp.ssreflect.finfun]
-finfun_cons [constructor, in mathcomp.ssreflect.finfun]
-finfun_nil [constructor, in mathcomp.ssreflect.finfun]
-finfun_on [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]
-finMixin [definition, in mathcomp.ssreflect.finfun]
-finmodule [library]
-finPi [abbreviation, in mathcomp.ssreflect.finfun]
-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.alg_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_countZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_finType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.alg_countType [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.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.countType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.countZmodType [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.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.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.comRing_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.comRing_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.comRing_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.comRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.comRing_finType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countComRing_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countComRing_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countComRing_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countComRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countComRing_finType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.countZmodType [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.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.choiceType [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.comRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRing_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRing_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRing_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRing_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.comUnitRing_finType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRing_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRing_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRing_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRing_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countComUnitRing_finType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countUnitRing_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.countZmodType [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.finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.finComRing_finUnitRingType [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.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.unitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.unitRing_finComRingType [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.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.countComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countFieldType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finIdomainType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countField_finType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countIdomainType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.countZmodType [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.field_finIdomainType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_finComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.field_finType [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.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.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.countComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomainType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_finComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countIdomain_finType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.countZmodType [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.idomain_finComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.idomain_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.idomain_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.idomain_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.idomain_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.idomain_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.idomain_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.idomain_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.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.countType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.countZmodType [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.finLmod_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.finLmod_countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.finLmod_ringType [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.lalgType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_countZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_finType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lalg_countType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lmod_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.lmod_countRingType [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.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.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.countZmodType [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.lmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.lmod_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.lmod_countZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.lmod_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.lmod_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.lmod_finType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.lmod_countType [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.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.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.countRing_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.countRing_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.countRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.countRing_finType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.countType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.countZmodType [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.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.ring_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.ring_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.ring_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.ring_finType [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.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.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countUnitRing_finAlgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countUnitRing_algType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countUnitRing_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countUnitRing_lalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countUnitRing_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countUnitRing_lmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.countZmodType [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.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.finUnitRing_finAlgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.finUnitRing_algType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.finUnitRing_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.finUnitRing_lalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.finUnitRing_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.finUnitRing_lmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.lalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.lmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.mixin [projection, 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.unitAlgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finAlgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_countUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_countZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_finType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitAlg_countType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitRing_finAlgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitRing_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.unitRing_finLmodType [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.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.countRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countUnitRing_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countUnitRing_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countUnitRing_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countUnitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countUnitRing_finType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.countZmodType [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.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.unitRing_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.unitRing_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.unitRing_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.unitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.unitRing_finType [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.countZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.countZmod_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.countZmod_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.countZmod_finType [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.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.Zmodule.zmod_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.zmod_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.zmod_finType [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]
-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]
-foldlE [lemma, in mathcomp.ssreflect.bigop]
-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]
-foldl_idx [lemma, in mathcomp.ssreflect.bigop]
-foldr [definition, in mathcomp.ssreflect.seq]
-foldrE [lemma, in mathcomp.ssreflect.bigop]
-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_inPP [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]
-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]
-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]
-FunPlainTheory [section, in mathcomp.ssreflect.finfun]
-FunPlainTheory.aT [variable, in mathcomp.ssreflect.finfun]
-FunPlainTheory.rT [variable, in mathcomp.ssreflect.finfun]
-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 [definition, in mathcomp.ssreflect.finfun]
-fun_of_fin_rec [definition, 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -