F (Lemmas)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
F (Lemmas)
f_finv [prf, in mathcomp.boot.fingraph]f_finv_cycle [prf, in mathcomp.boot.fingraph]
f_finv_in [prf, in mathcomp.boot.fingraph]
f_iinv [prf, in mathcomp.boot.fintype]
f_invF [prf, in mathcomp.boot.fintype]
F_r012 [prf, in mathcomp.solvable.burnside_app]
F_r013 [prf, in mathcomp.solvable.burnside_app]
F_r021 [prf, in mathcomp.solvable.burnside_app]
F_r024 [prf, in mathcomp.solvable.burnside_app]
F_r031 [prf, in mathcomp.solvable.burnside_app]
F_r034 [prf, in mathcomp.solvable.burnside_app]
F_r042 [prf, in mathcomp.solvable.burnside_app]
F_r043 [prf, in mathcomp.solvable.burnside_app]
F_r05 [prf, in mathcomp.solvable.burnside_app]
F_r1 [prf, in mathcomp.solvable.burnside_app]
F_r14 [prf, in mathcomp.solvable.burnside_app]
F_r2 [prf, in mathcomp.solvable.burnside_app]
F_r23 [prf, in mathcomp.solvable.burnside_app]
F_r3 [prf, in mathcomp.solvable.burnside_app]
F_r32 [prf, in mathcomp.solvable.burnside_app]
F_r41 [prf, in mathcomp.solvable.burnside_app]
F_r50 [prf, in mathcomp.solvable.burnside_app]
F_s05 [prf, in mathcomp.solvable.burnside_app]
F_s1 [prf, in mathcomp.solvable.burnside_app]
F_s14 [prf, in mathcomp.solvable.burnside_app]
F_s2 [prf, in mathcomp.solvable.burnside_app]
F_s23 [prf, in mathcomp.solvable.burnside_app]
F_s3 [prf, in mathcomp.solvable.burnside_app]
F_s4 [prf, in mathcomp.solvable.burnside_app]
F_s5 [prf, in mathcomp.solvable.burnside_app]
F_s6 [prf, in mathcomp.solvable.burnside_app]
F_Sd1 [prf, in mathcomp.solvable.burnside_app]
F_Sd2 [prf, in mathcomp.solvable.burnside_app]
F_Sh [prf, in mathcomp.solvable.burnside_app]
F_Sv [prf, in mathcomp.solvable.burnside_app]
fact0 [prf, in mathcomp.boot.ssrnat]
fact_geq [prf, in mathcomp.boot.ssrnat]
fact_gt0 [prf, in mathcomp.boot.ssrnat]
fact_prod [prf, in mathcomp.boot.binomial]
fact_split [prf, in mathcomp.boot.binomial]
factE [prf, in mathcomp.boot.ssrnat]
factm_morphM [prf, in mathcomp.finite_group.morphism]
factmE [prf, in mathcomp.finite_group.morphism]
factmod_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
factmod_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
factor_theorem [prf, in mathcomp.algebra.poly]
factor_Xn_sub_1 [prf, in mathcomp.algebra.poly]
factS [prf, in mathcomp.boot.ssrnat]
Fadjoin0 [prf, in mathcomp.field.fieldext]
Fadjoin1_polyP [prf, in mathcomp.field.fieldext]
Fadjoin_eq_sum [prf, in mathcomp.field.fieldext]
Fadjoin_idP [prf, in mathcomp.field.fieldext]
Fadjoin_nil [prf, in mathcomp.field.fieldext]
Fadjoin_poly_eq [prf, in mathcomp.field.fieldext]
Fadjoin_poly_is_linear [prf, in mathcomp.field.fieldext]
Fadjoin_poly_mod [prf, in mathcomp.field.fieldext]
Fadjoin_poly_unique [prf, in mathcomp.field.fieldext]
Fadjoin_polyC [prf, in mathcomp.field.fieldext]
Fadjoin_polyOver [prf, in mathcomp.field.fieldext]
Fadjoin_polyP [prf, in mathcomp.field.fieldext]
Fadjoin_polyX [prf, in mathcomp.field.fieldext]
Fadjoin_seqP [prf, in mathcomp.field.fieldext]
Fadjoin_sum_direct [prf, in mathcomp.field.fieldext]
FadjoinP [prf, in mathcomp.field.fieldext]
faithful_degree_p_part [prf, in mathcomp.group_representation.integral_char]
faithful_isom [prf, in mathcomp.finite_group.action]
faithful_repr_extraspecial_pchar [prf, in mathcomp.group_representation.mxabelem]
faithfulP [prf, in mathcomp.finite_group.action]
faithfulR [prf, in mathcomp.finite_group.action]
Falgebra_FieldMixin [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_compE [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_invE [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_invr_out [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_mulE [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_mulrRV [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_mulrV [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_mulRVr [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_mulVr [prf, in mathcomp.field.falgebra]
FalgLfun.lfun_unitrP [prf, in mathcomp.field.falgebra]
FalgType_proper [prf, in mathcomp.field.falgebra]
familyP [prf, in mathcomp.boot.finfun]
fcard_finv [prf, in mathcomp.boot.fingraph]
fcard_gt0P [prf, in mathcomp.boot.fingraph]
fcard_gt1P [prf, in mathcomp.boot.fingraph]
fcard_id [prf, in mathcomp.boot.fingraph]
fcard_order_set [prf, in mathcomp.boot.fingraph]
fclosed1 [prf, in mathcomp.boot.fingraph]
fconnect1 [prf, in mathcomp.boot.fingraph]
fconnect_cycle [prf, in mathcomp.boot.fingraph]
fconnect_eqVf [prf, in mathcomp.boot.fingraph]
fconnect_f [prf, in mathcomp.boot.fingraph]
fconnect_findex [prf, in mathcomp.boot.fingraph]
fconnect_finv [prf, in mathcomp.boot.fingraph]
fconnect_id [prf, in mathcomp.boot.fingraph]
fconnect_invariant [prf, in mathcomp.boot.fingraph]
fconnect_iter [prf, in mathcomp.boot.fingraph]
fconnect_orbit [prf, in mathcomp.boot.fingraph]
fconnect_sym [prf, in mathcomp.boot.fingraph]
fconnect_sym_in [prf, in mathcomp.boot.fingraph]
fcycle_consE [prf, in mathcomp.boot.fingraph]
fcycle_consEflatten [prf, in mathcomp.boot.fingraph]
fcycle_rconsE [prf, in mathcomp.boot.fingraph]
fcycle_undup [prf, in mathcomp.boot.fingraph]
fcycleEflatten [prf, in mathcomp.boot.fingraph]
Fermat's_little_theorem [prf, in mathcomp.field.finfield]
fermat_little [prf, in mathcomp.boot.binomial]
ffact0n [prf, in mathcomp.boot.binomial]
ffact_fact [prf, in mathcomp.boot.binomial]
ffact_factd [prf, in mathcomp.boot.binomial]
ffact_gt0 [prf, in mathcomp.boot.binomial]
ffact_prod [prf, in mathcomp.boot.binomial]
ffact_small [prf, in mathcomp.boot.binomial]
ffactE [prf, in mathcomp.boot.binomial]
ffactn0 [prf, in mathcomp.boot.binomial]
ffactn1 [prf, in mathcomp.boot.binomial]
ffactnn [prf, in mathcomp.boot.binomial]
ffactnS [prf, in mathcomp.boot.binomial]
ffactnSr [prf, in mathcomp.boot.binomial]
ffactSS [prf, in mathcomp.boot.binomial]
fful_lin_char_inj [prf, in mathcomp.group_representation.character]
ffun0 [prf, in mathcomp.boot.finfun]
ffun1_nonzero [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_add0r [prf, in mathcomp.boot.nmodule]
ffun_addNr [prf, in mathcomp.boot.nmodule]
ffun_addrA [prf, in mathcomp.boot.nmodule]
ffun_addrC [prf, in mathcomp.boot.nmodule]
ffun_mul1g [prf, in mathcomp.boot.monoid]
ffun_mul_0l [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mul_0r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mul_1l [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mul_1r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mul_addl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mul_addr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mulA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mulC [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_mulg1 [prf, in mathcomp.boot.monoid]
ffun_mulgA [prf, in mathcomp.boot.monoid]
ffun_mulgV [prf, in mathcomp.boot.monoid]
ffun_mulVg [prf, in mathcomp.boot.monoid]
ffun_onP [prf, in mathcomp.boot.finfun]
ffun_scale0r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_scale1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_scale_addl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_scale_addr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_scaleA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ffun_vect_iso [prf, in mathcomp.algebra.vector]
ffunE [prf, in mathcomp.boot.finfun]
ffunK [prf, in mathcomp.boot.finfun]
ffunMnE [prf, in mathcomp.boot.nmodule]
ffunMzE [prf, in mathcomp.algebra.ssrint]
ffunP [prf, in mathcomp.boot.finfun]
fgraph_codom [prf, in mathcomp.boot.finfun]
fgraph_ffun0 [prf, in mathcomp.boot.finfun]
fgraphK [prf, in mathcomp.boot.finfun]
Fid [prf, in mathcomp.solvable.burnside_app]
Fid3 [prf, in mathcomp.solvable.burnside_app]
field_dimS [prf, in mathcomp.field.fieldext]
field_mem_algid [prf, in mathcomp.field.fieldext]
field_module_dimS [prf, in mathcomp.field.fieldext]
field_module_eq [prf, in mathcomp.field.fieldext]
field_module_semisimple [prf, in mathcomp.field.fieldext]
field_mul_group_cyclic [prf, in mathcomp.solvable.cyclic]
field_subvMl [prf, in mathcomp.field.fieldext]
field_subvMr [prf, in mathcomp.field.fieldext]
field_unit_group_cyclic [prf, in mathcomp.solvable.cyclic]
fieldExt_hornerC [prf, in mathcomp.field.fieldext]
fieldExt_hornerX [prf, in mathcomp.field.fieldext]
fieldExt_hornerZ [prf, in mathcomp.field.fieldext]
fieldOver_scale1 [prf, in mathcomp.field.fieldext]
fieldOver_scaleA [prf, in mathcomp.field.fieldext]
fieldOver_scaleAl [prf, in mathcomp.field.fieldext]
fieldOver_scaleDl [prf, in mathcomp.field.fieldext]
fieldOver_scaleDr [prf, in mathcomp.field.fieldext]
fieldOver_scaleE [prf, in mathcomp.field.fieldext]
fieldOver_splitting [prf, in mathcomp.field.galois]
fieldOver_vectMixin [prf, in mathcomp.field.fieldext]
filter_all [prf, in mathcomp.boot.seq]
filter_cat [prf, in mathcomp.boot.seq]
filter_flatten [prf, in mathcomp.boot.seq]
filter_free [prf, in mathcomp.algebra.vector]
filter_id [prf, in mathcomp.boot.seq]
filter_iota_leq [prf, in mathcomp.boot.seq]
filter_iota_ltn [prf, in mathcomp.boot.seq]
filter_map [prf, in mathcomp.boot.seq]
filter_mask [prf, in mathcomp.boot.seq]
filter_nseq [prf, in mathcomp.boot.seq]
filter_pairwise_orthogonal [prf, in mathcomp.group_representation.classfun]
filter_pairwise_orthogonal [prf, in mathcomp.algebra.sesquilinear]
filter_pi_of [prf, in mathcomp.boot.prime]
filter_pred0 [prf, in mathcomp.boot.seq]
filter_pred1_uniq [prf, in mathcomp.boot.seq]
filter_predI [prf, in mathcomp.boot.seq]
filter_predT [prf, in mathcomp.boot.seq]
filter_rcons [prf, in mathcomp.boot.seq]
filter_rev [prf, in mathcomp.boot.seq]
filter_sort [prf, in mathcomp.boot.path]
filter_sort_in [prf, in mathcomp.boot.path]
filter_subseq [prf, in mathcomp.boot.seq]
filter_subset [prf, in mathcomp.boot.fintype]
filter_undup [prf, in mathcomp.boot.seq]
filter_uniq [prf, in mathcomp.boot.seq]
fin_all_exists [prf, in mathcomp.boot.fintype]
fin_all_exists2 [prf, in mathcomp.boot.fintype]
fin_Csubring_Aint [prf, in mathcomp.field.algnum]
fin_Fp_lmod_abelem [prf, in mathcomp.solvable.abelian]
fin_lmod_pchar_abelem [prf, in mathcomp.solvable.abelian]
fin_pickleK [prf, in mathcomp.boot.fintype]
fin_ring_pchar_abelem [prf, in mathcomp.solvable.abelian]
find_cat [prf, in mathcomp.boot.seq]
find_ex_minn [prf, in mathcomp.boot.ssrnat]
find_ltn [prf, in mathcomp.boot.seq]
find_map [prf, in mathcomp.boot.seq]
find_nseq [prf, in mathcomp.boot.seq]
find_pred0 [prf, in mathcomp.boot.seq]
find_predT [prf, in mathcomp.boot.seq]
find_size [prf, in mathcomp.boot.seq]
findex0 [prf, in mathcomp.boot.fingraph]
findex_eq0 [prf, in mathcomp.boot.fingraph]
findex_iter [prf, in mathcomp.boot.fingraph]
findex_max [prf, in mathcomp.boot.fingraph]
finDomain_field [prf, in mathcomp.field.finfield]
finDomain_mulrC [prf, in mathcomp.field.finfield]
findP [prf, in mathcomp.boot.seq]
finField_galois [prf, in mathcomp.field.finfield]
finField_galois_generator [prf, in mathcomp.field.finfield]
finField_genPoly [prf, in mathcomp.field.finfield]
finField_is_abelem [prf, in mathcomp.field.finfield]
finfun_of_tupleK [prf, in mathcomp.boot.finfun]
FinfunK [prf, in mathcomp.boot.finfun]
finite_PET [prf, in mathcomp.field.separable]
FiniteModule.act0r [prf, in mathcomp.solvable.finmodule]
FiniteModule.actAr [prf, in mathcomp.solvable.finmodule]
FiniteModule.actNr [prf, in mathcomp.solvable.finmodule]
FiniteModule.actr1 [prf, in mathcomp.solvable.finmodule]
FiniteModule.actr_is_action [prf, in mathcomp.solvable.finmodule]
FiniteModule.actr_is_groupAction [prf, in mathcomp.solvable.finmodule]
FiniteModule.actrK [prf, in mathcomp.solvable.finmodule]
FiniteModule.actrKV [prf, in mathcomp.solvable.finmodule]
FiniteModule.actrM [prf, in mathcomp.solvable.finmodule]
FiniteModule.actZr [prf, in mathcomp.solvable.finmodule]
FiniteModule.congr_fmod [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmod1 [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmod_add0r [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmod_addNr [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmod_addrA [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmod_addrC [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmod_inj [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmodJ [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmodK [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmodKcond [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmodM [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmodP [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmodV [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmodX [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmval0 [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmvalA [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmvalJ [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmvalJcond [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmvalK [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmvalN [prf, in mathcomp.solvable.finmodule]
FiniteModule.fmvalZ [prf, in mathcomp.solvable.finmodule]
FiniteModule.injm_fmod [prf, in mathcomp.solvable.finmodule]
FiniteNES.Finite.count_enumP [prf, in mathcomp.boot.fintype]
FiniteNES.Finite.uniq_enumP [prf, in mathcomp.boot.fintype]
finNzRing_gt1 [prf, in mathcomp.field.finfield]
finNzRing_nontrivial [prf, in mathcomp.field.finfield]
finPcharP [prf, in mathcomp.field.finfield]
FinRing.Builders_221.decidable [prf, in mathcomp.algebra.finalg]
FinRing.Builders_48.intro_unit [prf, in mathcomp.algebra.finalg]
FinRing.Builders_48.invr_out [prf, in mathcomp.algebra.finalg]
FinRing.Builders_48.mulrV [prf, in mathcomp.algebra.finalg]
FinRing.Builders_48.mulVr [prf, in mathcomp.algebra.finalg]
FinRing.unit_actE [prf, in mathcomp.algebra.finalg]
FinRing.unit_inv_proof [prf, in mathcomp.algebra.finalg]
FinRing.unit_is_groupAction [prf, in mathcomp.algebra.finalg]
FinRing.unit_mul1u [prf, in mathcomp.algebra.finalg]
FinRing.unit_mul_proof [prf, in mathcomp.algebra.finalg]
FinRing.unit_muluA [prf, in mathcomp.algebra.finalg]
FinRing.unit_mulVu [prf, in mathcomp.algebra.finalg]
FinRing.val_unit1 [prf, in mathcomp.algebra.finalg]
FinRing.val_unitM [prf, in mathcomp.algebra.finalg]
FinRing.val_unitV [prf, in mathcomp.algebra.finalg]
FinRing.val_unitX [prf, in mathcomp.algebra.finalg]
FinRing.zmod1gE [prf, in mathcomp.algebra.finalg]
FinRing.zmod_abelian [prf, in mathcomp.algebra.finalg]
FinRing.zmod_mulgC [prf, in mathcomp.algebra.finalg]
FinRing.zmodMgE [prf, in mathcomp.algebra.finalg]
FinRing.zmodVgE [prf, in mathcomp.algebra.finalg]
FinRing.zmodXgE [prf, in mathcomp.algebra.finalg]
FinSplittingFieldFor [prf, in mathcomp.field.finfield]
FinTuple.enumP [prf, in mathcomp.boot.tuple]
FinTuple.size_enum [prf, in mathcomp.boot.tuple]
fintype0 [prf, in mathcomp.boot.fintype]
fintype1 [prf, in mathcomp.boot.fintype]
fintype1P [prf, in mathcomp.boot.fintype]
fintype_le1P [prf, in mathcomp.boot.fintype]
finv_bij [prf, in mathcomp.boot.fingraph]
finv_cycle [prf, in mathcomp.boot.fingraph]
finv_eq_can [prf, in mathcomp.boot.fingraph]
finv_f [prf, in mathcomp.boot.fingraph]
finv_f_cycle [prf, in mathcomp.boot.fingraph]
finv_f_in [prf, in mathcomp.boot.fingraph]
finv_in [prf, in mathcomp.boot.fingraph]
finv_inj [prf, in mathcomp.boot.fingraph]
finv_inj_cycle [prf, in mathcomp.boot.fingraph]
finv_inj_in [prf, in mathcomp.boot.fingraph]
finv_inv [prf, in mathcomp.boot.fingraph]
first_isog [prf, in mathcomp.finite_group.quotient]
first_isog_loc [prf, in mathcomp.finite_group.quotient]
first_isom [prf, in mathcomp.finite_group.quotient]
first_isom_loc [prf, in mathcomp.finite_group.quotient]
first_orthogonality_relation [prf, in mathcomp.group_representation.character]
Fitting_char [prf, in mathcomp.solvable.maximal]
Fitting_eq_pcore [prf, in mathcomp.solvable.maximal]
Fitting_group_set [prf, in mathcomp.solvable.maximal]
Fitting_max [prf, in mathcomp.solvable.maximal]
Fitting_nil [prf, in mathcomp.solvable.maximal]
Fitting_normal [prf, in mathcomp.solvable.maximal]
Fitting_pcore [prf, in mathcomp.solvable.maximal]
Fitting_sub [prf, in mathcomp.solvable.maximal]
FittingEgen [prf, in mathcomp.solvable.maximal]
FittingJ [prf, in mathcomp.solvable.maximal]
FittingS [prf, in mathcomp.solvable.maximal]
fix_order_big [prf, in mathcomp.boot.finset]
fix_order_eq0 [prf, in mathcomp.boot.finset]
fix_order_gt0 [prf, in mathcomp.boot.finset]
fix_order_le_max [prf, in mathcomp.boot.finset]
fix_order_proof [prf, in mathcomp.boot.finset]
fix_order_small [prf, in mathcomp.boot.finset]
fixed_gal [prf, in mathcomp.field.galois]
fixedField_bound [prf, in mathcomp.field.galois]
fixedField_galois [prf, in mathcomp.field.galois]
fixedField_is_aspace [prf, in mathcomp.field.galois]
fixedFieldP [prf, in mathcomp.field.galois]
fixedFieldS [prf, in mathcomp.field.galois]
fixedPoly_gal [prf, in mathcomp.field.galois]
fixedSpace_id [prf, in mathcomp.algebra.vector]
fixedSpace_limg [prf, in mathcomp.algebra.vector]
fixedSpaceP [prf, in mathcomp.algebra.vector]
fixedSpacesP [prf, in mathcomp.algebra.vector]
fixsetK [prf, in mathcomp.boot.finset]
fixsetKn [prf, in mathcomp.boot.finset]
flatmx0 [prf, in mathcomp.algebra.matrix]
flatmxOver [prf, in mathcomp.algebra.matrix]
flatten_cat [prf, in mathcomp.boot.seq]
flatten_imageP [prf, in mathcomp.boot.fintype]
flatten_indexKl [prf, in mathcomp.boot.seq]
flatten_indexKr [prf, in mathcomp.boot.seq]
flatten_indexP [prf, in mathcomp.boot.seq]
flatten_map1 [prf, in mathcomp.boot.seq]
flatten_mapP [prf, in mathcomp.boot.seq]
flatten_rcons [prf, in mathcomp.boot.seq]
flatten_seq1 [prf, in mathcomp.boot.seq]
flattenK [prf, in mathcomp.boot.seq]
flattenP [prf, in mathcomp.boot.seq]
floor_rat [prf, in mathcomp.algebra.rat]
floorErat [prf, in mathcomp.algebra.rat]
fmorph_eq_rat [prf, in mathcomp.algebra.rat]
fmorph_numZ [prf, in mathcomp.field.algnum]
fmorph_primitive_root [prf, in mathcomp.algebra.poly]
fmorph_rat [prf, in mathcomp.algebra.rat]
fmorph_root [prf, in mathcomp.algebra.poly]
fmorph_unity_root [prf, in mathcomp.algebra.poly]
fmorphXz [prf, in mathcomp.algebra.ssrint]
foldl_cat [prf, in mathcomp.boot.seq]
foldl_foldr [prf, in mathcomp.boot.seq]
foldl_idx [prf, in mathcomp.boot.bigop]
foldl_rcons [prf, in mathcomp.boot.seq]
foldl_rev [prf, in mathcomp.boot.seq]
foldlE [prf, in mathcomp.boot.bigop]
foldr_cat [prf, in mathcomp.boot.seq]
foldr_map [prf, in mathcomp.boot.seq]
foldr_rcons [prf, in mathcomp.boot.seq]
foldrE [prf, in mathcomp.boot.bigop]
forall_cons [prf, in mathcomp.boot.seq]
forall_inP [prf, in mathcomp.boot.fintype]
forall_inPn [prf, in mathcomp.boot.fintype]
forall_inPP [prf, in mathcomp.boot.fintype]
forallb_tnth [prf, in mathcomp.boot.tuple]
forallP [prf, in mathcomp.boot.fintype]
forallPn [prf, in mathcomp.boot.fintype]
forallPP [prf, in mathcomp.boot.fintype]
form0_eq0 [prf, in mathcomp.algebra.sesquilinear]
form0l [prf, in mathcomp.algebra.sesquilinear]
form0r [prf, in mathcomp.algebra.sesquilinear]
form1_row_schmidt [prf, in mathcomp.algebra.spectral]
form_eq0C [prf, in mathcomp.algebra.sesquilinear]
form_eq0P [prf, in mathcomp.algebra.sesquilinear]
form_of_matrix_is_bilinear [prf, in mathcomp.algebra.sesquilinear]
form_of_matrix_is_hermitian [prf, in mathcomp.algebra.sesquilinear]
form_of_matrixK [prf, in mathcomp.algebra.sesquilinear]
form_sign [prf, in mathcomp.algebra.sesquilinear]
formB [prf, in mathcomp.algebra.sesquilinear]
formBd [prf, in mathcomp.algebra.sesquilinear]
formC [prf, in mathcomp.algebra.sesquilinear]
formD [prf, in mathcomp.algebra.sesquilinear]
formDd [prf, in mathcomp.algebra.sesquilinear]
formDl [prf, in mathcomp.algebra.sesquilinear]
formDr [prf, in mathcomp.algebra.sesquilinear]
formee [prf, in mathcomp.algebra.sesquilinear]
formN [prf, in mathcomp.algebra.sesquilinear]
formNl [prf, in mathcomp.algebra.sesquilinear]
formNr [prf, in mathcomp.algebra.sesquilinear]
formZ [prf, in mathcomp.algebra.sesquilinear]
formZl [prf, in mathcomp.algebra.sesquilinear]
formZr [prf, in mathcomp.algebra.sesquilinear]
Fp_cast [prf, in mathcomp.algebra.zmodp]
Fp_fieldMixin [prf, in mathcomp.algebra.zmodp]
Fp_nat_mod [prf, in mathcomp.algebra.zmodp]
Fp_Zcast [prf, in mathcomp.algebra.zmodp]
fpath_f_finv_cycle [prf, in mathcomp.boot.fingraph]
fpath_f_finv_in [prf, in mathcomp.boot.fingraph]
fpath_finv [prf, in mathcomp.boot.fingraph]
fpath_finv_cycle [prf, in mathcomp.boot.fingraph]
fpath_finv_f_cycle [prf, in mathcomp.boot.fingraph]
fpath_finv_f_in [prf, in mathcomp.boot.fingraph]
fpath_finv_in [prf, in mathcomp.boot.fingraph]
fpath_traject [prf, in mathcomp.boot.path]
fpathE [prf, in mathcomp.boot.path]
fpathP [prf, in mathcomp.boot.path]
fprod_of_dffun_bij [prf, in mathcomp.boot.finfun]
fprod_of_dffunK [prf, in mathcomp.boot.finfun]
fprodE [prf, in mathcomp.boot.finfun]
fprodK [prf, in mathcomp.boot.finfun]
fprodP [prf, in mathcomp.boot.finfun]
frac0q [prf, in mathcomp.algebra.rat]
FracField.add0_l [prf, in mathcomp.algebra.fraction]
FracField.addA [prf, in mathcomp.algebra.fraction]
FracField.addC [prf, in mathcomp.algebra.fraction]
FracField.addN_l [prf, in mathcomp.algebra.fraction]
FracField.equivf_def [prf, in mathcomp.algebra.fraction]
FracField.equivf_l [prf, in mathcomp.algebra.fraction]
FracField.equivf_r [prf, in mathcomp.algebra.fraction]
FracField.equivf_refl [prf, in mathcomp.algebra.fraction]
FracField.equivf_sym [prf, in mathcomp.algebra.fraction]
FracField.equivf_trans [prf, in mathcomp.algebra.fraction]
FracField.equivfE [prf, in mathcomp.algebra.fraction]
FracField.inv0 [prf, in mathcomp.algebra.fraction]
FracField.mul1_l [prf, in mathcomp.algebra.fraction]
FracField.mul_addl [prf, in mathcomp.algebra.fraction]
FracField.mulA [prf, in mathcomp.algebra.fraction]
FracField.mulC [prf, in mathcomp.algebra.fraction]
FracField.mulV_l [prf, in mathcomp.algebra.fraction]
FracField.nonzero1 [prf, in mathcomp.algebra.fraction]
FracField.numer0 [prf, in mathcomp.algebra.fraction]
FracField.pi_add [prf, in mathcomp.algebra.fraction]
FracField.pi_inv [prf, in mathcomp.algebra.fraction]
FracField.pi_mul [prf, in mathcomp.algebra.fraction]
FracField.pi_opp [prf, in mathcomp.algebra.fraction]
FracField.Ratio_numden [prf, in mathcomp.algebra.fraction]
fracq0 [prf, in mathcomp.algebra.rat]
fracq_eq [prf, in mathcomp.algebra.rat]
fracq_eq0 [prf, in mathcomp.algebra.rat]
fracq_opt_subdef_id [prf, in mathcomp.algebra.rat]
fracq_opt_subdefE [prf, in mathcomp.algebra.rat]
fracqE [prf, in mathcomp.algebra.rat]
fracqMM [prf, in mathcomp.algebra.rat]
fracqP [prf, in mathcomp.algebra.rat]
Frattini_arg [prf, in mathcomp.solvable.sylow]
Frattini_continuous [prf, in mathcomp.solvable.maximal]
free_cons [prf, in mathcomp.algebra.vector]
free_directv [prf, in mathcomp.algebra.vector]
free_not0 [prf, in mathcomp.algebra.vector]
free_span [prf, in mathcomp.algebra.vector]
free_uniq [prf, in mathcomp.algebra.vector]
freeE [prf, in mathcomp.algebra.vector]
freeNE [prf, in mathcomp.algebra.vector]
freeP [prf, in mathcomp.algebra.vector]
Frobenius_action_kernel_def [prf, in mathcomp.solvable.frobenius]
Frobenius_actionP [prf, in mathcomp.solvable.frobenius]
Frobenius_Cauchy [prf, in mathcomp.finite_group.action]
Frobenius_cent1_ker [prf, in mathcomp.solvable.frobenius]
Frobenius_compl_Hall [prf, in mathcomp.solvable.frobenius]
Frobenius_context [prf, in mathcomp.solvable.frobenius]
Frobenius_coprime [prf, in mathcomp.solvable.frobenius]
Frobenius_coprime_quotient [prf, in mathcomp.solvable.frobenius]
Frobenius_dvd_ker1 [prf, in mathcomp.solvable.frobenius]
Frobenius_Ind_irrP [prf, in mathcomp.group_representation.inertia]
Frobenius_index_coprime [prf, in mathcomp.solvable.frobenius]
Frobenius_index_dvd_ker1 [prf, in mathcomp.solvable.frobenius]
Frobenius_ker_coprime [prf, in mathcomp.solvable.frobenius]
Frobenius_ker_dvd_ker1 [prf, in mathcomp.solvable.frobenius]
Frobenius_ker_Hall [prf, in mathcomp.solvable.frobenius]
Frobenius_kernel_exists [prf, in mathcomp.group_representation.vcharacter]
Frobenius_kerP [prf, in mathcomp.solvable.frobenius]
Frobenius_kerS [prf, in mathcomp.solvable.frobenius]
Frobenius_Ldiv [prf, in mathcomp.solvable.frobenius]
Frobenius_partition [prf, in mathcomp.solvable.frobenius]
Frobenius_reciprocity [prf, in mathcomp.group_representation.classfun]
Frobenius_reg_compl [prf, in mathcomp.solvable.frobenius]
Frobenius_reg_ker [prf, in mathcomp.solvable.frobenius]
Frobenius_semiregularP [prf, in mathcomp.solvable.frobenius]
Frobenius_subl [prf, in mathcomp.solvable.frobenius]
Frobenius_subr [prf, in mathcomp.solvable.frobenius]
Frobenius_trivg_cent [prf, in mathcomp.solvable.frobenius]
FrobeniusJ [prf, in mathcomp.solvable.frobenius]
FrobeniusJcompl [prf, in mathcomp.solvable.frobenius]
FrobeniusJgroup [prf, in mathcomp.solvable.frobenius]
FrobeniusJker [prf, in mathcomp.solvable.frobenius]
FrobeniusW [prf, in mathcomp.solvable.frobenius]
FrobeniusWcompl [prf, in mathcomp.solvable.frobenius]
FrobeniusWker [prf, in mathcomp.solvable.frobenius]
froot_id [prf, in mathcomp.boot.fingraph]
froots_id [prf, in mathcomp.boot.fingraph]
fst_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
fst_is_multiplicative [prf, in mathcomp.boot.monoid]
fst_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
fst_is_umagma_morphism [prf, in mathcomp.boot.monoid]
fst_is_zmod_morphism [prf, in mathcomp.boot.nmodule]
fst_morphM [prf, in mathcomp.finite_group.gproduct]
ftaggedE [prf, in mathcomp.boot.finset]
fullrankfun_inj [prf, in mathcomp.algebra.mxalgebra]
fullrowsub_free [prf, in mathcomp.algebra.mxalgebra]
fullrowsub_full [prf, in mathcomp.algebra.mxalgebra]
fullrowsub_unit [prf, in mathcomp.algebra.mxalgebra]
fullv_lfunP [prf, in mathcomp.algebra.vector]
fun_of_lfunK [prf, in mathcomp.algebra.vector]
Fundamental_Theorem_of_Algebraics [prf, in mathcomp.field.algebraics_fundamentals]
funsetC_mono [prf, in mathcomp.boot.finset]