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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## F

fact [definition, in ssrnat]factm [definition, in morphisms]

factmE [lemma, in morphisms]

factm_morphism [definition, in morphisms]

factm_morphM [lemma, in morphisms]

FactorMorphism [section, in morphisms]

FactorMorphism.aT [variable, in morphisms]

FactorMorphism.f [variable, in morphisms]

FactorMorphism.G [variable, in morphisms]

FactorMorphism.H [variable, in morphisms]

FactorMorphism.q [variable, in morphisms]

FactorMorphism.qT [variable, in morphisms]

FactorMorphism.rT [variable, in morphisms]

FactorMorphism.sGH [variable, in morphisms]

FactorMorphism.sKqKf [variable, in morphisms]

factor0 [lemma, in poly]

factor_theorem [lemma, in poly]

factS [lemma, in binomial]

fact0 [lemma, in binomial]

fact_gt0 [lemma, in ssrnat]

fact_pos_nat [definition, in ssrnat]

fact_prod [lemma, in binomial]

family [definition, in finfun]

familyP [lemma, in finfun]

fB [abbreviation, in morphisms]

fcard_finv [lemma, in connect]

fclosed1 [lemma, in connect]

FconnectEq [section, in connect]

FconnectEq.Eff' [variable, in connect]

FconnectEq.f [variable, in connect]

FconnectEq.f' [variable, in connect]

FconnectEq.Hf [variable, in connect]

FconnectEq.T [variable, in connect]

fconnect1 [lemma, in connect]

fconnect_cycle [lemma, in connect]

fconnect_finv [lemma, in connect]

fconnect_invariant [lemma, in connect]

fconnect_iter [lemma, in connect]

fconnect_orbit [lemma, in connect]

fconnect_sym [lemma, in connect]

ff [abbreviation, in morphisms]

ffT [abbreviation, in finfun]

ffunE [lemma, in finfun]

ffunK [lemma, in finfun]

ffunP [lemma, in finfun]

ffun_on [definition, in finfun]

ffun_onP [lemma, in finfun]

fgraph [definition, in finfun]

fgraph_map [lemma, in finfun]

fH [abbreviation, in normal]

fH_G [abbreviation, in normal]

Field [module, in ssralg]

FieldIdomainMixin [abbreviation, in ssralg]

FieldMixin [abbreviation, in ssralg]

FieldMulCyclic [section, in cyclic]

FieldMulCyclic.G [variable, in cyclic]

FieldMulCyclic.gT [variable, in cyclic]

FieldType [abbreviation, in ssralg]

fieldType [abbreviation, in ssralg]

FieldUnitMixin [abbreviation, in ssralg]

field_mul_group_cyclic [lemma, in cyclic]

filter [definition, in seq]

filter_cat [lemma, in seq]

filter_index_enum [lemma, in bigops]

filter_map [lemma, in seq]

filter_pi_of [lemma, in prime]

filter_predI [lemma, in seq]

filter_predT [lemma, in seq]

filter_pred0 [lemma, in seq]

filter_rcons [lemma, in seq]

filter_sieve [lemma, in seq]

filter_uniq [lemma, in seq]

FinCancel [section, in fintype]

FinCancel [section, in connect]

FinCancel.Ef [variable, in connect]

FinCancel.f [variable, in connect]

FinCancel.f [variable, in fintype]

FinCancel.fK [variable, in fintype]

FinCancel.f' [variable, in connect]

FinCancel.g [variable, in fintype]

FinCancel.Inv [section, in fintype]

FinCancel.Inv.injf [variable, in fintype]

FinCancel.T [variable, in fintype]

FinCancel.T [variable, in connect]

find [definition, in seq]

findex [definition, in connect]

findex0 [lemma, in connect]

findex_iter [lemma, in connect]

findex_max [lemma, in connect]

find_cat [lemma, in seq]

find_ex_minn [lemma, in ssrnat]

find_map [lemma, in seq]

find_size [lemma, in seq]

finEnum_unlock [definition, in fintype]

Finfun [constructor, in finfun]

finfun [abbreviation, in finfun]

finfun [library]

finfun_choiceMixin [definition, in finfun]

finfun_choiceType [definition, in finfun]

finfun_countMixin [definition, in finfun]

finfun_countType [definition, in finfun]

finfun_def [abbreviation, in finfun]

finfun_eqMixin [definition, in finfun]

finfun_eqType [definition, in finfun]

finfun_finMixin [definition, in finfun]

finfun_finType [definition, in finfun]

finfun_of [definition, in finfun]

finfun_of_choiceType [definition, in finfun]

finfun_of_countType [definition, in finfun]

finfun_of_eqType [definition, in finfun]

finfun_of_finType [definition, in finfun]

finfun_of_set [definition, in finset]

finfun_of_subCountType [definition, in finfun]

finfun_of_subFinType [definition, in finfun]

finfun_of_subType [definition, in finfun]

finfun_subCountType [definition, in finfun]

finfun_subFinType [definition, in finfun]

finfun_subType [definition, in finfun]

finfun_type [inductive, in finfun]

finfun_unlock [definition, in finfun]

FinGroup [module, in groups]

FinGroupType [abbreviation, in groups]

finGroupType [abbreviation, in groups]

FinGroup.arg_sort [definition, in groups]

FinGroup.base [projection, in groups]

FinGroup.BaseMixin [constructor, in groups]

FinGroup.base_type [record, in groups]

FinGroup.finClass [definition, in groups]

FinGroup.inv [projection, in groups]

FinGroup.Mixin [section, in groups]

FinGroup.mixin [definition, in groups]

FinGroup.Mixin [definition, in groups]

FinGroup.Mixin.inv [variable, in groups]

FinGroup.Mixin.mul [variable, in groups]

FinGroup.Mixin.mulA [variable, in groups]

FinGroup.Mixin.mulV [variable, in groups]

FinGroup.Mixin.mul1 [variable, in groups]

FinGroup.Mixin.one [variable, in groups]

FinGroup.Mixin.T [variable, in groups]

FinGroup.mixin_of [record, in groups]

FinGroup.mk_invgK [lemma, in groups]

FinGroup.mk_invMg [lemma, in groups]

FinGroup.mul [projection, in groups]

FinGroup.one [projection, in groups]

FinGroup.Pack [constructor, in groups]

FinGroup.PackBase [constructor, in groups]

FinGroup.pack_base [definition, in groups]

FinGroup.repack [definition, in groups]

FinGroup.repack_arg [definition, in groups]

FinGroup.repack_base [definition, in groups]

FinGroup.sort [projection, in groups]

FinGroup.type [record, in groups]

finGroup_arg_choiceType [definition, in groups]

finGroup_arg_countType [definition, in groups]

finGroup_arg_eqType [definition, in groups]

finGroup_arg_finType [definition, in groups]

finGroup_choiceType [definition, in groups]

finGroup_countType [definition, in groups]

finGroup_eqType [definition, in groups]

finGroup_finType [definition, in groups]

finGroup_law [definition, in groups]

Finite [module, in fintype]

Finite.axiom [definition, in fintype]

Finite.base [projection, in fintype]

Finite.choiceType [definition, in fintype]

Finite.class [definition, in fintype]

Finite.Class [constructor, in fintype]

Finite.class_of [record, in fintype]

Finite.CountAxiom [section, in fintype]

Finite.CountAxiom.n [variable, in fintype]

Finite.CountAxiom.T [variable, in fintype]

Finite.CountAxiom.ubT [variable, in fintype]

Finite.CountMixin [definition, in fintype]

Finite.countType [definition, in fintype]

Finite.count_enum [definition, in fintype]

Finite.count_enumP [lemma, in fintype]

Finite.enum [abbreviation, in fintype]

Finite.EnumDef.enum [definition, in fintype]

Finite.EnumDef.enumDef [definition, in fintype]

Finite.EnumSig.enum [axiom, in fintype]

Finite.EnumSig.enumDef [axiom, in fintype]

Finite.eqType [definition, in fintype]

Finite.mixin [projection, in fintype]

Finite.Mixin [constructor, in fintype]

Finite.mixin_enum [projection, in fintype]

Finite.mixin_of [record, in fintype]

Finite.Pack [constructor, in fintype]

Finite.pack [definition, in fintype]

Finite.repack [definition, in fintype]

Finite.sort [projection, in fintype]

Finite.type [record, in fintype]

Finite.UniqMixin [definition, in fintype]

Finite.uniq_enumP [lemma, in fintype]

Finite.unpack [definition, in fintype]

FinMixin [abbreviation, in fintype]

FinPowerSet [section, in finfun]

FinPowerSet.A [variable, in finfun]

FinPowerSet.eT [variable, in finfun]

finset [abbreviation, in finset]

FinSet [constructor, in finset]

finset [library]

finset_def [abbreviation, in finset]

finset_unlock [definition, in finset]

FinTheory [section, in finfun]

FinTheory.aT [variable, in finfun]

FinTheory.rT [variable, in finfun]

FinTuple [module, in tuple]

FinTupleSig [module, in tuple]

FinTupleSig.enum [axiom, in tuple]

FinTupleSig.enumP [axiom, in tuple]

FinTupleSig.FinTupleSig [section, in tuple]

FinTupleSig.FinTupleSig.n [variable, in tuple]

FinTupleSig.FinTupleSig.T [variable, in tuple]

FinTupleSig.size_enum [axiom, in tuple]

FinTuple.enum [definition, in tuple]

FinTuple.enumP [lemma, in tuple]

FinTuple.FinTuple [section, in tuple]

FinTuple.FinTuple.n [variable, in tuple]

FinTuple.FinTuple.T [variable, in tuple]

FinTuple.size_enum [lemma, in tuple]

FinType [abbreviation, in fintype]

finType [abbreviation, in fintype]

fintype [library]

FinTypeForSub [section, in fintype]

FinTypeForSub.P [variable, in fintype]

FinTypeForSub.sT [variable, in fintype]

FinTypeForSub.T [variable, in fintype]

finv [definition, in connect]

finv_bij [lemma, in connect]

finv_eq_can [lemma, in connect]

finv_f [lemma, in connect]

finv_inj [lemma, in connect]

finv_inv [lemma, in connect]

fin_inj_bij [lemma, in connect]

FirstIsomorphism [section, in normal]

FirstIsomorphism.aT [variable, in normal]

FirstIsomorphism.f [variable, in normal]

FirstIsomorphism.G [variable, in normal]

FirstIsomorphism.H [variable, in normal]

FirstIsomorphism.rT [variable, in normal]

FirstIsomorphism.sHG [variable, in normal]

first_isog [lemma, in normal]

first_isog_loc [lemma, in normal]

first_isom [lemma, in normal]

first_isom_loc [lemma, in normal]

Flatten [section, in seq]

flatten [definition, in seq]

flattenK [lemma, in seq]

Flatten.T [variable, in seq]

fm [abbreviation, in automorphism]

fmE [abbreviation, in automorphism]

fMT [abbreviation, in morphisms]

foldl [definition, in seq]

FoldLeft [section, in seq]

FoldLeft.f [variable, in seq]

FoldLeft.R [variable, in seq]

FoldLeft.T [variable, in seq]

foldl_cat [lemma, in seq]

foldl_rev [lemma, in seq]

foldr [definition, in seq]

FoldRight [section, in seq]

FoldRightComp [section, in seq]

FoldRightComp.f [variable, in seq]

FoldRightComp.h [variable, in seq]

FoldRightComp.R [variable, in seq]

FoldRightComp.T1 [variable, in seq]

FoldRightComp.T2 [variable, in seq]

FoldRightComp.z0 [variable, in seq]

FoldRight.f [variable, in seq]

FoldRight.R [variable, in seq]

FoldRight.T [variable, in seq]

FoldRight.z0 [variable, in seq]

foldr_cat [lemma, in seq]

foldr_map [lemma, in seq]

forallP [lemma, in fintype]

fpathP [lemma, in paths]

fpath_finv [lemma, in connect]

fpath_traject [lemma, in paths]

Fp_field [definition, in zmodp]

Fp_fieldMixin [lemma, in zmodp]

Fp_idomainMixin [definition, in zmodp]

Fp_ring [definition, in zmodp]

frefl [lemma, in ssrfun]

frel [definition, in eqtype]

fsym [lemma, in ssrfun]

fT [abbreviation, in finfun]

fT [abbreviation, in finfun]

fT [abbreviation, in finfun]

ftrans [lemma, in ssrfun]

FunDelta [constructor, in eqtype]

FunFinfun [module, in finfun]

FunFinfunSig [module, in finfun]

FunFinfunSig.finfun [axiom, in finfun]

FunFinfunSig.finfunE [axiom, in finfun]

FunFinfunSig.fun_of_fin [axiom, in finfun]

FunFinfunSig.fun_of_finE [axiom, in finfun]

FunFinfun.finfun [definition, in finfun]

FunFinfun.finfunE [lemma, in finfun]

FunFinfun.fun_of_fin [definition, in finfun]

FunFinfun.fun_of_finE [lemma, in finfun]

FunImage [section, in finset]

FunImageComp [section, in finset]

FunImageComp.T [variable, in finset]

FunImageComp.T' [variable, in finset]

FunImageComp.U [variable, in finset]

FunImage.aT [variable, in finset]

FunImage.aT2 [variable, in finset]

FunImage.ImsetTheory [section, in finset]

FunImage.ImsetTheory.ImsetProp [section, in finset]

FunImage.ImsetTheory.ImsetProp.f [variable, in finset]

FunImage.ImsetTheory.ImsetProp.f2 [variable, in finset]

FunImage.ImsetTheory.rT [variable, in finset]

FunWith [section, in eqtype]

FunWith.aT [variable, in eqtype]

FunWith.rT [variable, in eqtype]

Fun2Set1 [section, in finset]

Fun2Set1.aT1 [variable, in finset]

Fun2Set1.aT2 [variable, in finset]

Fun2Set1.f [variable, in finset]

Fun2Set1.rT [variable, in finset]

fun_adjunction [definition, in connect]

fun_base [definition, in paths]

fun_delta [inductive, in eqtype]

fun_if [lemma, in ssrbool]

fun_of_fin [abbreviation, in finfun]

fun_of_fin_def [abbreviation, in finfun]

fun_of_fin_unlock [definition, in finfun]

fun_of_matrix [definition, in matrix]

fun_of_perm [abbreviation, in perm]

fun_of_perm_def [abbreviation, in perm]

fun_of_perm_unlock [definition, in perm]

fun_of_simpl [definition, in ssrfun]

fwith [definition, in eqtype]

f_finv [lemma, in connect]

f_iinv [lemma, in fintype]

f_invF [lemma, in fintype]

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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |