I (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 |
I (Lemmas)
id_is_ahom [prf, in mathcomp.field.falgebra]id_lfunE [prf, in mathcomp.algebra.vector]
idealMr [prf, in mathcomp.algebra.ring_quotient]
idealr0 [prf, in mathcomp.algebra.ring_quotient]
idealr1 [prf, in mathcomp.algebra.ring_quotient]
idealr_closed_nontrivial [prf, in mathcomp.algebra.ring_quotient]
idealr_closedB [prf, in mathcomp.algebra.ring_quotient]
idem_sub_le_big [prf, in mathcomp.boot.bigop]
idem_sub_le_big_cond [prf, in mathcomp.boot.bigop]
idfun_gmulf1 [prf, in mathcomp.boot.monoid]
idfun_gmulfM [prf, in mathcomp.boot.monoid]
idGfun_closed [prf, in mathcomp.solvable.gfunctor]
idGfun_cont [prf, in mathcomp.solvable.gfunctor]
idGfun_monotonic [prf, in mathcomp.solvable.gfunctor]
idm_isom [prf, in mathcomp.finite_group.morphism]
idm_morphM [prf, in mathcomp.finite_group.morphism]
idmxE [prf, in mathcomp.algebra.matrix]
ieexprIz [prf, in mathcomp.algebra.ssrint]
if_add [prf, in mathcomp.boot.ssrbool]
if_and [prf, in mathcomp.boot.ssrbool]
if_implyb [prf, in mathcomp.boot.ssrbool]
if_implybC [prf, in mathcomp.boot.ssrbool]
if_nth [prf, in mathcomp.boot.seq]
if_or [prf, in mathcomp.boot.ssrbool]
ifactmE [prf, in mathcomp.finite_group.morphism]
ifN_eq [prf, in mathcomp.boot.eqtype]
ifN_eqC [prf, in mathcomp.boot.eqtype]
iinv_f [prf, in mathcomp.boot.fintype]
iinv_proof [prf, in mathcomp.boot.fintype]
Iirr1_neq0 [prf, in mathcomp.group_representation.character]
Iirr_cast [prf, in mathcomp.group_representation.character]
im_abelem_rV [prf, in mathcomp.group_representation.mxabelem]
im_actm [prf, in mathcomp.finite_group.action]
im_actperm_Aut [prf, in mathcomp.finite_group.action]
im_Aut_isom [prf, in mathcomp.finite_group.automorphism]
im_autm [prf, in mathcomp.finite_group.automorphism]
im_cfclass_Iirr [prf, in mathcomp.group_representation.inertia]
im_coset [prf, in mathcomp.finite_group.quotient]
im_cpair [prf, in mathcomp.solvable.center]
im_cpair_cent [prf, in mathcomp.solvable.center]
im_cpair_cprod [prf, in mathcomp.solvable.center]
im_cprodm [prf, in mathcomp.finite_group.gproduct]
im_cyclem [prf, in mathcomp.solvable.cyclic]
im_dprodm [prf, in mathcomp.finite_group.gproduct]
im_eltm [prf, in mathcomp.solvable.cyclic]
im_idm [prf, in mathcomp.finite_group.morphism]
im_ifactm [prf, in mathcomp.finite_group.morphism]
im_invm [prf, in mathcomp.finite_group.morphism]
im_perm_on [prf, in mathcomp.finite_group.perm]
im_permV [prf, in mathcomp.finite_group.perm]
im_qisom [prf, in mathcomp.finite_group.quotient]
im_qisom_proof [prf, in mathcomp.finite_group.quotient]
im_quotient [prf, in mathcomp.finite_group.quotient]
im_restr_perm [prf, in mathcomp.finite_group.action]
im_restrm [prf, in mathcomp.finite_group.morphism]
im_rVabelem [prf, in mathcomp.group_representation.mxabelem]
im_sdpair [prf, in mathcomp.finite_group.gproduct]
im_sdpair_norm [prf, in mathcomp.finite_group.gproduct]
im_sdpair_TI [prf, in mathcomp.finite_group.gproduct]
im_sdprodm [prf, in mathcomp.finite_group.gproduct]
im_sdprodm1 [prf, in mathcomp.finite_group.gproduct]
im_sdprodm2 [prf, in mathcomp.finite_group.gproduct]
im_sgval [prf, in mathcomp.finite_group.morphism]
im_subg [prf, in mathcomp.finite_group.morphism]
im_transversal_repr [prf, in mathcomp.boot.finset]
im_xcprodm [prf, in mathcomp.solvable.center]
im_xcprodml [prf, in mathcomp.solvable.center]
im_xcprodmr [prf, in mathcomp.solvable.center]
im_xsdprodm [prf, in mathcomp.finite_group.gproduct]
im_Zp_unitm [prf, in mathcomp.solvable.cyclic]
im_Zpm [prf, in mathcomp.solvable.cyclic]
image_codom [prf, in mathcomp.boot.fintype]
image_f [prf, in mathcomp.boot.fintype]
image_iinv [prf, in mathcomp.boot.fintype]
image_injP [prf, in mathcomp.boot.fintype]
image_orbit [prf, in mathcomp.boot.fingraph]
image_pre [prf, in mathcomp.boot.fintype]
image_pred0 [prf, in mathcomp.boot.fintype]
imageP [prf, in mathcomp.boot.fintype]
Immx_rect [prf, in mathcomp.algebra.spectral]
imset0 [prf, in mathcomp.boot.finset]
imset0mem [prf, in mathcomp.boot.finset]
imset2_f [prf, in mathcomp.boot.finset]
imset2_pair [prf, in mathcomp.boot.finset]
imset2_set1l [prf, in mathcomp.boot.finset]
imset2_set1r [prf, in mathcomp.boot.finset]
imset2P [prf, in mathcomp.boot.finset]
imset2S [prf, in mathcomp.boot.finset]
imset2Sl [prf, in mathcomp.boot.finset]
imset2Sr [prf, in mathcomp.boot.finset]
imset2Ul [prf, in mathcomp.boot.finset]
imset2Ur [prf, in mathcomp.boot.finset]
imset_autE [prf, in mathcomp.finite_group.automorphism]
imset_card [prf, in mathcomp.boot.finset]
imset_comp [prf, in mathcomp.boot.finset]
imset_coset [prf, in mathcomp.finite_group.quotient]
imset_cover [prf, in mathcomp.boot.finset]
imset_disjoint [prf, in mathcomp.boot.finset]
imset_eq0 [prf, in mathcomp.boot.finset]
imset_f [prf, in mathcomp.boot.finset]
imset_id [prf, in mathcomp.boot.finset]
imset_inj [prf, in mathcomp.boot.finset]
imset_injP [prf, in mathcomp.boot.finset]
imset_mulgm [prf, in mathcomp.finite_group.gproduct]
imset_partition [prf, in mathcomp.boot.finset]
imset_perm1 [prf, in mathcomp.finite_group.perm]
imset_proper [prf, in mathcomp.boot.finset]
imset_set1 [prf, in mathcomp.boot.finset]
imset_trivIset [prf, in mathcomp.boot.finset]
imsetI [prf, in mathcomp.boot.finset]
imsetP [prf, in mathcomp.boot.finset]
imsetS [prf, in mathcomp.boot.finset]
imsetU [prf, in mathcomp.boot.finset]
imsetU1 [prf, in mathcomp.boot.finset]
in_alg_comm [prf, in mathcomp.algebra.poly]
in_bseqE [prf, in mathcomp.boot.tuple]
in_cons [prf, in mathcomp.boot.seq]
in_cprodM [prf, in mathcomp.solvable.center]
in_factmod_addsK [prf, in mathcomp.group_representation.mxrepresentation]
in_factmod_eq0 [prf, in mathcomp.group_representation.mxrepresentation]
in_factmod_module [prf, in mathcomp.group_representation.mxrepresentation]
in_factmodE [prf, in mathcomp.group_representation.mxrepresentation]
in_factmodJ [prf, in mathcomp.group_representation.mxrepresentation]
in_factmodK [prf, in mathcomp.group_representation.mxrepresentation]
in_factmodsK [prf, in mathcomp.group_representation.mxrepresentation]
in_iinv_f [prf, in mathcomp.boot.fintype]
in_iter [prf, in mathcomp.boot.finset]
in_iter_fix_orderE [prf, in mathcomp.boot.finset]
in_iter_fixE [prf, in mathcomp.boot.finset]
in_itv [prf, in mathcomp.algebra.interval]
in_itvI [prf, in mathcomp.algebra.interval]
in_mask [prf, in mathcomp.boot.seq]
in_nil [prf, in mathcomp.boot.seq]
in_one_group [prf, in mathcomp.finite_group.fingroup]
in_orbit [prf, in mathcomp.boot.fingraph]
in_orbit_cycle [prf, in mathcomp.boot.fingraph]
in_qpoly0 [prf, in mathcomp.algebra.qpoly]
in_qpoly1 [prf, in mathcomp.algebra.qpoly]
in_qpoly_comp_horner [prf, in mathcomp.field.qfpoly]
in_qpoly_is_linear [prf, in mathcomp.algebra.qpoly]
in_qpoly_monoid_morphism [prf, in mathcomp.algebra.qpoly]
in_qpoly_small [prf, in mathcomp.algebra.qpoly]
in_qpolyD [prf, in mathcomp.algebra.qpoly]
in_qpolyM [prf, in mathcomp.algebra.qpoly]
in_qpolyZ [prf, in mathcomp.algebra.qpoly]
in_set [prf, in mathcomp.boot.finset]
in_set0 [prf, in mathcomp.boot.finset]
in_set1 [prf, in mathcomp.boot.finset]
in_set2 [prf, in mathcomp.boot.finset]
in_setC [prf, in mathcomp.boot.finset]
in_setC1 [prf, in mathcomp.boot.finset]
in_setD [prf, in mathcomp.boot.finset]
in_setD1 [prf, in mathcomp.boot.finset]
in_setI [prf, in mathcomp.boot.finset]
in_setT [prf, in mathcomp.boot.finset]
in_setU [prf, in mathcomp.boot.finset]
in_setU1 [prf, in mathcomp.boot.finset]
in_setX [prf, in mathcomp.boot.finset]
in_setXn [prf, in mathcomp.boot.finset]
in_submod_eq0 [prf, in mathcomp.group_representation.mxrepresentation]
in_submod_module [prf, in mathcomp.group_representation.mxrepresentation]
in_submodE [prf, in mathcomp.group_representation.mxrepresentation]
in_submodJ [prf, in mathcomp.group_representation.mxrepresentation]
in_submodK [prf, in mathcomp.group_representation.mxrepresentation]
in_take [prf, in mathcomp.boot.seq]
in_take_leq [prf, in mathcomp.boot.seq]
in_tuple_cons [prf, in mathcomp.boot.tuple]
in_tuple_tuple [prf, in mathcomp.boot.tuple]
in_tupleE [prf, in mathcomp.boot.tuple]
in_tupleP [prf, in mathcomp.boot.tuple]
incn_inj [prf, in mathcomp.boot.ssrnat]
incn_inj_in [prf, in mathcomp.boot.ssrnat]
incr_nth_inj [prf, in mathcomp.boot.seq]
incr_nthC [prf, in mathcomp.boot.seq]
incr_tallyP [prf, in mathcomp.boot.seq]
Ind_irr_neq0 [prf, in mathcomp.group_representation.character]
index1g [prf, in mathcomp.finite_group.fingroup]
index2_normal [prf, in mathcomp.finite_group.fingroup]
index_cat [prf, in mathcomp.boot.seq]
index_cent1 [prf, in mathcomp.finite_group.action]
index_cosetpre [prf, in mathcomp.finite_group.quotient]
index_enum_key [prf, in mathcomp.boot.bigop]
index_enum_ord [prf, in mathcomp.boot.fintype]
index_enum_uniq [prf, in mathcomp.boot.bigop]
index_head [prf, in mathcomp.boot.seq]
index_inj [prf, in mathcomp.boot.seq]
index_injm [prf, in mathcomp.finite_group.quotient]
index_last [prf, in mathcomp.boot.seq]
index_ltn [prf, in mathcomp.boot.seq]
index_map [prf, in mathcomp.boot.seq]
index_map_in [prf, in mathcomp.boot.seq]
index_map_inW [prf, in mathcomp.boot.seq]
index_maxnormal_sol_prime [prf, in mathcomp.solvable.maximal]
index_mem [prf, in mathcomp.boot.seq]
index_morphim [prf, in mathcomp.finite_group.quotient]
index_morphim_ker [prf, in mathcomp.finite_group.quotient]
index_morphpre [prf, in mathcomp.finite_group.quotient]
index_nth [prf, in mathcomp.boot.seq]
index_pivot [prf, in mathcomp.boot.seq]
index_quotient [prf, in mathcomp.finite_group.quotient]
index_quotient_eq [prf, in mathcomp.finite_group.quotient]
index_quotient_ker [prf, in mathcomp.finite_group.quotient]
index_sdprod [prf, in mathcomp.finite_group.gproduct]
index_sdprodr [prf, in mathcomp.finite_group.gproduct]
index_size [prf, in mathcomp.boot.seq]
index_support_dvd_degree [prf, in mathcomp.group_representation.integral_char]
index_uniq [prf, in mathcomp.boot.seq]
indexed_partition [prf, in mathcomp.boot.finset]
indexg1 [prf, in mathcomp.finite_group.fingroup]
indexg_eq1 [prf, in mathcomp.finite_group.fingroup]
indexg_gt0 [prf, in mathcomp.finite_group.fingroup]
indexg_gt1 [prf, in mathcomp.finite_group.fingroup]
indexgg [prf, in mathcomp.finite_group.fingroup]
indexgI [prf, in mathcomp.finite_group.fingroup]
indexgS [prf, in mathcomp.finite_group.fingroup]
indexJg [prf, in mathcomp.finite_group.fingroup]
indexMg [prf, in mathcomp.finite_group.fingroup]
indexSg [prf, in mathcomp.finite_group.fingroup]
inertia0 [prf, in mathcomp.group_representation.inertia]
Inertia1 [prf, in mathcomp.group_representation.inertia]
inertia1 [prf, in mathcomp.group_representation.inertia]
inertia_add [prf, in mathcomp.group_representation.inertia]
inertia_bigdprod [prf, in mathcomp.group_representation.inertia]
inertia_bigdprod_irr [prf, in mathcomp.group_representation.inertia]
inertia_bigdprodi [prf, in mathcomp.group_representation.inertia]
inertia_dprod [prf, in mathcomp.group_representation.inertia]
inertia_dprod_irr [prf, in mathcomp.group_representation.inertia]
inertia_dprodl [prf, in mathcomp.group_representation.inertia]
inertia_dprodr [prf, in mathcomp.group_representation.inertia]
inertia_Frobenius_ker [prf, in mathcomp.group_representation.inertia]
inertia_id [prf, in mathcomp.group_representation.inertia]
inertia_injective [prf, in mathcomp.group_representation.inertia]
inertia_irr0 [prf, in mathcomp.group_representation.inertia]
inertia_irr_prime [prf, in mathcomp.group_representation.inertia]
inertia_isom [prf, in mathcomp.group_representation.inertia]
inertia_mod_pre [prf, in mathcomp.group_representation.inertia]
inertia_mod_quo [prf, in mathcomp.group_representation.inertia]
inertia_morph_im [prf, in mathcomp.group_representation.inertia]
inertia_morph_pre [prf, in mathcomp.group_representation.inertia]
inertia_mul [prf, in mathcomp.group_representation.inertia]
inertia_opp [prf, in mathcomp.group_representation.inertia]
inertia_prod [prf, in mathcomp.group_representation.inertia]
inertia_quo [prf, in mathcomp.group_representation.inertia]
inertia_scale [prf, in mathcomp.group_representation.inertia]
inertia_scale_nz [prf, in mathcomp.group_representation.inertia]
inertia_sdprod [prf, in mathcomp.group_representation.inertia]
Inertia_sub [prf, in mathcomp.group_representation.inertia]
inertia_sum [prf, in mathcomp.group_representation.inertia]
inertia_valJ [prf, in mathcomp.group_representation.inertia]
inertiaJ [prf, in mathcomp.group_representation.inertia]
infix0s [prf, in mathcomp.boot.seq]
infix1s [prf, in mathcomp.boot.seq]
infix_catl [prf, in mathcomp.boot.seq]
infix_catr [prf, in mathcomp.boot.seq]
infix_cons [prf, in mathcomp.boot.seq]
infix_consl [prf, in mathcomp.boot.seq]
infix_drop [prf, in mathcomp.boot.seq]
infix_index0s [prf, in mathcomp.boot.seq]
infix_index_le [prf, in mathcomp.boot.seq]
infix_indexs0 [prf, in mathcomp.boot.seq]
infix_indexss [prf, in mathcomp.boot.seq]
infix_infix [prf, in mathcomp.boot.seq]
infix_prefix_trans [prf, in mathcomp.boot.seq]
infix_rcons [prf, in mathcomp.boot.seq]
infix_rconsl [prf, in mathcomp.boot.seq]
infix_refl [prf, in mathcomp.boot.seq]
infix_rev [prf, in mathcomp.boot.seq]
infix_revLR [prf, in mathcomp.boot.seq]
infix_sorted [prf, in mathcomp.boot.path]
infix_suffix_trans [prf, in mathcomp.boot.seq]
infix_take [prf, in mathcomp.boot.seq]
infix_trans [prf, in mathcomp.boot.seq]
infix_uniq [prf, in mathcomp.boot.seq]
infixE [prf, in mathcomp.boot.seq]
infixP [prf, in mathcomp.boot.seq]
infixPn [prf, in mathcomp.boot.seq]
infixs0 [prf, in mathcomp.boot.seq]
infixs1 [prf, in mathcomp.boot.seq]
infixTindex [prf, in mathcomp.boot.seq]
infixW [prf, in mathcomp.boot.seq]
inj_card_bij [prf, in mathcomp.boot.fintype]
inj_card_onto [prf, in mathcomp.boot.fintype]
inj_cycle [prf, in mathcomp.boot.path]
inj_eq [prf, in mathcomp.boot.eqtype]
inj_eqAxiom [prf, in mathcomp.boot.eqtype]
inj_homo [prf, in mathcomp.boot.eqtype]
inj_homo_in [prf, in mathcomp.boot.eqtype]
inj_homo_ltn [prf, in mathcomp.boot.ssrnat]
inj_homo_ltn_in [prf, in mathcomp.boot.ssrnat]
inj_in_eq [prf, in mathcomp.boot.eqtype]
inj_in_map [prf, in mathcomp.boot.seq]
inj_leq [prf, in mathcomp.boot.fintype]
inj_map [prf, in mathcomp.boot.seq]
inj_nhomo_ltn [prf, in mathcomp.boot.ssrnat]
inj_nhomo_ltn_in [prf, in mathcomp.boot.ssrnat]
inj_omap [prf, in mathcomp.boot.ssrfun]
inj_onth_map [prf, in mathcomp.boot.seq]
inj_row_free [prf, in mathcomp.algebra.mxalgebra]
inj_tperm [prf, in mathcomp.finite_group.perm]
injectiveP [prf, in mathcomp.boot.fintype]
injectivePcycle [prf, in mathcomp.boot.fingraph]
injectivePn [prf, in mathcomp.boot.fintype]
injF_bij [prf, in mathcomp.boot.fintype]
injF_onto [prf, in mathcomp.boot.fintype]
injm1 [prf, in mathcomp.finite_group.morphism]
injm_abelem [prf, in mathcomp.solvable.abelian]
injm_abelian [prf, in mathcomp.finite_group.morphism]
injm_actm [prf, in mathcomp.finite_group.action]
injm_Aut [prf, in mathcomp.finite_group.automorphism]
injm_Aut_full [prf, in mathcomp.finite_group.action]
injm_Aut_isom [prf, in mathcomp.finite_group.automorphism]
injm_Aut_sub [prf, in mathcomp.finite_group.action]
injm_autm [prf, in mathcomp.finite_group.automorphism]
injm_bigdprod [prf, in mathcomp.finite_group.gproduct]
injm_cent [prf, in mathcomp.finite_group.morphism]
injm_cent1 [prf, in mathcomp.finite_group.morphism]
injm_center [prf, in mathcomp.solvable.center]
injm_cents [prf, in mathcomp.finite_group.morphism]
injm_char [prf, in mathcomp.finite_group.automorphism]
injm_comp [prf, in mathcomp.finite_group.morphism]
injm_conj [prf, in mathcomp.finite_group.automorphism]
injm_cpair1g [prf, in mathcomp.solvable.center]
injm_cpairg1 [prf, in mathcomp.solvable.center]
injm_cprodm [prf, in mathcomp.finite_group.gproduct]
injm_cyclem [prf, in mathcomp.solvable.cyclic]
injm_cyclic [prf, in mathcomp.solvable.cyclic]
injm_dfung1 [prf, in mathcomp.finite_group.gproduct]
injm_dprod [prf, in mathcomp.finite_group.gproduct]
injm_dprodm [prf, in mathcomp.finite_group.gproduct]
injm_eltm [prf, in mathcomp.solvable.cyclic]
injm_eq [prf, in mathcomp.finite_group.morphism]
injm_extraspecial [prf, in mathcomp.solvable.maximal]
injm_factm [prf, in mathcomp.finite_group.morphism]
injm_factmP [prf, in mathcomp.finite_group.morphism]
injm_faithful [prf, in mathcomp.finite_group.action]
injm_Fitting [prf, in mathcomp.solvable.maximal]
injm_Frobenius [prf, in mathcomp.solvable.frobenius]
injm_Frobenius_compl [prf, in mathcomp.solvable.frobenius]
injm_Frobenius_group [prf, in mathcomp.solvable.frobenius]
injm_Frobenius_ker [prf, in mathcomp.solvable.frobenius]
injm_generator [prf, in mathcomp.solvable.cyclic]
injm_grank [prf, in mathcomp.solvable.abelian]
injm_idm [prf, in mathcomp.finite_group.morphism]
injm_ifactm [prf, in mathcomp.finite_group.morphism]
injm_invm [prf, in mathcomp.finite_group.morphism]
injm_Ldiv [prf, in mathcomp.solvable.abelian]
injm_maximal [prf, in mathcomp.solvable.gseries]
injm_maximal_eq [prf, in mathcomp.solvable.gseries]
injm_maxnormal [prf, in mathcomp.solvable.gseries]
injm_minnormal [prf, in mathcomp.solvable.gseries]
injm_morphim_inj [prf, in mathcomp.finite_group.morphism]
injm_nElem [prf, in mathcomp.solvable.abelian]
injm_nil [prf, in mathcomp.solvable.nilpotent]
injm_norm [prf, in mathcomp.finite_group.morphism]
injm_normal [prf, in mathcomp.finite_group.morphism]
injm_norms [prf, in mathcomp.finite_group.morphism]
injm_Ohm [prf, in mathcomp.solvable.abelian]
injm_p_rank [prf, in mathcomp.solvable.abelian]
injm_pair1g [prf, in mathcomp.finite_group.gproduct]
injm_pairg1 [prf, in mathcomp.finite_group.gproduct]
injm_pcore [prf, in mathcomp.solvable.pgroup]
injm_pElem [prf, in mathcomp.solvable.abelian]
injm_pelt [prf, in mathcomp.solvable.pgroup]
injm_pgroup [prf, in mathcomp.solvable.pgroup]
injm_pHall [prf, in mathcomp.solvable.pgroup]
injm_Phi [prf, in mathcomp.solvable.maximal]
injm_pmaxElem [prf, in mathcomp.solvable.abelian]
injm_pnElem [prf, in mathcomp.solvable.abelian]
injm_pprodm [prf, in mathcomp.finite_group.gproduct]
injm_proper [prf, in mathcomp.finite_group.morphism]
injm_pseries [prf, in mathcomp.solvable.pgroup]
injm_qisom [prf, in mathcomp.finite_group.quotient]
injm_quotm [prf, in mathcomp.finite_group.quotient]
injm_rank [prf, in mathcomp.solvable.abelian]
injm_restrm [prf, in mathcomp.finite_group.morphism]
injm_sdpair1 [prf, in mathcomp.finite_group.gproduct]
injm_sdpair2 [prf, in mathcomp.finite_group.gproduct]
injm_sdprod [prf, in mathcomp.finite_group.gproduct]
injm_sdprodm [prf, in mathcomp.finite_group.gproduct]
injm_sgval [prf, in mathcomp.finite_group.morphism]
injm_sol [prf, in mathcomp.solvable.nilpotent]
injm_special [prf, in mathcomp.solvable.maximal]
injm_subcent [prf, in mathcomp.finite_group.morphism]
injm_subcent1 [prf, in mathcomp.finite_group.morphism]
injm_subg [prf, in mathcomp.finite_group.morphism]
injm_subnorm [prf, in mathcomp.finite_group.morphism]
injm_ucn [prf, in mathcomp.solvable.nilpotent]
injm_xcprodm [prf, in mathcomp.solvable.center]
injm_xsdprodm [prf, in mathcomp.finite_group.gproduct]
injm_Zp_unitm [prf, in mathcomp.solvable.cyclic]
injm_Zpm [prf, in mathcomp.solvable.cyclic]
injmD1 [prf, in mathcomp.finite_group.morphism]
injmF [prf, in mathcomp.solvable.gfunctor]
injmF_sub [prf, in mathcomp.solvable.gfunctor]
injmI [prf, in mathcomp.finite_group.morphism]
injmK [prf, in mathcomp.finite_group.morphism]
injmP [prf, in mathcomp.finite_group.morphism]
injmSK [prf, in mathcomp.finite_group.morphism]
inl_inj [prf, in mathcomp.boot.ssrfun]
innew_val [prf, in mathcomp.boot.eqtype]
inord_val [prf, in mathcomp.boot.fintype]
inordK [prf, in mathcomp.boot.fintype]
inr_inj [prf, in mathcomp.boot.ssrfun]
inseparable_add [prf, in mathcomp.field.separable]
inseparable_sum [prf, in mathcomp.field.separable]
Instances.BRight_le_mul_boundr [prf, in mathcomp.algebra.interval_inference]
Instances.comparable_num_itv_bound [prf, in mathcomp.algebra.interval_inference]
Instances.nat_num_spec [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_add [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_double [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_exp [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_factorial [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_max [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_min [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_mul [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_succ [prf, in mathcomp.algebra.interval_inference]
Instances.nat_spec_zero [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_add_boundl [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_add_boundr [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_bound_exprn_le1 [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_bound_keep_neg [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_bound_keep_pos [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_bound_max [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_bound_min [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_mul_boundl [prf, in mathcomp.algebra.interval_inference]
Instances.num_itv_mul_boundr [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_add [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_exprn [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_exprz [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_int [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_intmul [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_inv [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_max [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_min [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_mul [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_natmul [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_Negz [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_norm [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_one [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_opp [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_Posz [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_sqrt [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_sqrtC [prf, in mathcomp.algebra.interval_inference]
Instances.num_spec_zero [prf, in mathcomp.algebra.interval_inference]
Instances.opp_boundl [prf, in mathcomp.algebra.interval_inference]
Instances.opp_boundr [prf, in mathcomp.algebra.interval_inference]
Instances.signP [prf, in mathcomp.algebra.interval_inference]
insub_eqE [prf, in mathcomp.boot.eqtype]
insubdK [prf, in mathcomp.boot.eqtype]
insubF [prf, in mathcomp.boot.eqtype]
insubK [prf, in mathcomp.boot.eqtype]
insubN [prf, in mathcomp.boot.eqtype]
insubP [prf, in mathcomp.boot.eqtype]
insubT [prf, in mathcomp.boot.eqtype]
int_rect [prf, in mathcomp.algebra.ssrint]
int_Smith_normal_form [prf, in mathcomp.algebra.intdiv]
IntDist.dist0n [prf, in mathcomp.algebra.ssrint]
IntDist.distn0 [prf, in mathcomp.algebra.ssrint]
IntDist.distn_eq0 [prf, in mathcomp.algebra.ssrint]
IntDist.distn_eq1 [prf, in mathcomp.algebra.ssrint]
IntDist.distnC [prf, in mathcomp.algebra.ssrint]
IntDist.distnDl [prf, in mathcomp.algebra.ssrint]
IntDist.distnDr [prf, in mathcomp.algebra.ssrint]
IntDist.distnEl [prf, in mathcomp.algebra.ssrint]
IntDist.distnEr [prf, in mathcomp.algebra.ssrint]
IntDist.distnn [prf, in mathcomp.algebra.ssrint]
IntDist.distnS [prf, in mathcomp.algebra.ssrint]
IntDist.distSn [prf, in mathcomp.algebra.ssrint]
IntDist.leqD_dist [prf, in mathcomp.algebra.ssrint]
IntDist.leqifD_dist [prf, in mathcomp.algebra.ssrint]
IntDist.leqifD_distz [prf, in mathcomp.algebra.ssrint]
IntDist.sqrn_dist [prf, in mathcomp.algebra.ssrint]
integral0 [prf, in mathcomp.algebra.mxpoly]
integral1 [prf, in mathcomp.algebra.mxpoly]
integral_add [prf, in mathcomp.algebra.mxpoly]
integral_algebraic [prf, in mathcomp.algebra.mxpoly]
integral_div [prf, in mathcomp.algebra.mxpoly]
integral_horner [prf, in mathcomp.algebra.mxpoly]
integral_horner_root [prf, in mathcomp.algebra.mxpoly]
integral_id [prf, in mathcomp.algebra.mxpoly]
integral_inv [prf, in mathcomp.algebra.mxpoly]
integral_mul [prf, in mathcomp.algebra.mxpoly]
integral_nat [prf, in mathcomp.algebra.mxpoly]
integral_opp [prf, in mathcomp.algebra.mxpoly]
integral_poly [prf, in mathcomp.algebra.mxpoly]
integral_rmorph [prf, in mathcomp.algebra.mxpoly]
integral_root [prf, in mathcomp.algebra.mxpoly]
integral_root_monic [prf, in mathcomp.algebra.mxpoly]
integral_sub [prf, in mathcomp.algebra.mxpoly]
Internals.add_pos_natE [prf, in mathcomp.algebra.ring_tactic]
Internals.add_termP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.addf_div_common [prf, in mathcomp.algebra.field_tactic]
Internals.BFormula_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.bool_R_eq [prf, in mathcomp.algebra.ring_tactic]
Internals.bool_Rxx [prf, in mathcomp.algebra.ring_tactic]
Internals.Cfield_checkerT [prf, in mathcomp.algebra.field_tactic]
Internals.check_inconsistentT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.check_normalised_formulasT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.cond_norm00_map_int_of_Z [prf, in mathcomp.algebra.field_tactic]
Internals.cond_norm2_map_int_of_Z [prf, in mathcomp.algebra.field_tactic]
Internals.Cring_checkerT [prf, in mathcomp.algebra.ring_tactic]
Internals.CTautoChecker_map_AC_of_C [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.CTautoCheckerT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Ctriv_divP [prf, in mathcomp.algebra.ring_tactic]
Internals.eKind_Rxx [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.env_jumpD [prf, in mathcomp.algebra.ring_tactic]
Internals.env_nth_jump [prf, in mathcomp.algebra.ring_tactic]
Internals.eq_bool_R [prf, in mathcomp.algebra.ring_tactic]
Internals.eq_bool_R2 [prf, in mathcomp.algebra.ring_tactic]
Internals.eq_Rnorm [prf, in mathcomp.algebra.ring_tactic]
Internals.erefl1 [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.erefl2 [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.erefl2b [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.erefl2n [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_and_cnf [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_cnf_ff [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_cnf_negate [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_cnf_normalise [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_cnf_of_GFormula [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_cnf_of_list [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_cnf_tt [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_eval_Psatz [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_negate_aux [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_nformula_plus_nformula [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_nformula_times_nformula [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_normalise_aux [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_OpAdd [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_OpMult [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_or_clause_cnf [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_or_cnf [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_or_cnf_aux [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_pexpr_times_nformula [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_rev_append [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.FEeval_map_int_of_Z [prf, in mathcomp.algebra.field_tactic]
Internals.FExpr_R_map [prf, in mathcomp.algebra.field_tactic]
Internals.field_checker_map_int_of_Z [prf, in mathcomp.algebra.field_tactic]
Internals.field_correct [prf, in mathcomp.algebra.field_tactic]
Internals.Formula_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.FTautoChecker_sound [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.hex_uint_N_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.is_boolP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.is_cnf_ffT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.is_cnf_ttT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.is_tautoT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.large_nat_N_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.list_R_eq [prf, in mathcomp.algebra.ring_tactic]
Internals.list_R_map [prf, in mathcomp.algebra.ring_tactic]
Internals.list_R_map2 [prf, in mathcomp.algebra.field_tactic]
Internals.list_Rxx [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Meval_MFactor [prf, in mathcomp.algebra.ring_tactic]
Internals.Meval_mk_monpol_list [prf, in mathcomp.algebra.ring_tactic]
Internals.Meval_mkVmon [prf, in mathcomp.algebra.ring_tactic]
Internals.Meval_mkZmon [prf, in mathcomp.algebra.ring_tactic]
Internals.Meval_Mon_of_Pol [prf, in mathcomp.algebra.ring_tactic]
Internals.Meval_zmon_pred [prf, in mathcomp.algebra.ring_tactic]
Internals.mulf_div_common [prf, in mathcomp.algebra.field_tactic]
Internals.N_R_eq [prf, in mathcomp.algebra.ring_tactic]
Internals.N_Rxx [prf, in mathcomp.algebra.ring_tactic]
Internals.N_to_natS [prf, in mathcomp.algebra.ring_tactic]
Internals.nat_of_N_expandE [prf, in mathcomp.algebra.ring_tactic]
Internals.nat_Rxx [prf, in mathcomp.algebra.ring_tactic]
Internals.Nat_tail_addE [prf, in mathcomp.algebra.ring_tactic]
Internals.Nat_tail_mulE [prf, in mathcomp.algebra.ring_tactic]
Internals.NFeval_normalise [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Nsemiring_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.nth_nth [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.numField_correct [prf, in mathcomp.algebra.field_tactic]
Internals.option_R_eq [prf, in mathcomp.algebra.field_tactic]
Internals.option_R_omap2 [prf, in mathcomp.algebra.field_tactic]
Internals.option_Rxx [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.or_clauseP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.PCond_app [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_cond_norm [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_cons [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_Fapp [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_Fcons0 [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_Fcons00 [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_Fcons1 [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_Fcons2 [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_Fnorm [prf, in mathcomp.algebra.field_tactic]
Internals.PCond_map_int_of_Z [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_default_isIn [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_eqs_map_int_of_Z [prf, in mathcomp.algebra.ring_tactic]
Internals.PEeval_eqs_map_N_to_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.PEeval_eqs_PEeval [prf, in mathcomp.algebra.ring_tactic]
Internals.PEeval_Fnorm [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_isIn [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_map_int_of_Z [prf, in mathcomp.algebra.ring_tactic]
Internals.PEeval_map_N_to_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.PEeval_NPEadd [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_NPEmul [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_NPEopp [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_NPEpow [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_NPEsub [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_PEsimp [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_split_aux [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_split_l [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_split_r [prf, in mathcomp.algebra.field_tactic]
Internals.PEmap_id [prf, in mathcomp.algebra.field_tactic]
Internals.Peval_addI [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_addX [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_CFactor [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_mkPinj [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_mkPX [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_mkX [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_mulC_aux [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_mulI [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_norm_subst [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_Peq [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_PNSubst [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_PNSubst1 [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_PNSubstL [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_Pol_of_PExpr [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_POneSubst [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_pow_N [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_pow_pos [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_PSubstL [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_PSubstL1 [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_square [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Peval_subI [prf, in mathcomp.algebra.ring_tactic]
Internals.Peval_subX [prf, in mathcomp.algebra.ring_tactic]
Internals.PevalB [prf, in mathcomp.algebra.ring_tactic]
Internals.PevalBC [prf, in mathcomp.algebra.ring_tactic]
Internals.PevalD [prf, in mathcomp.algebra.ring_tactic]
Internals.PevalDC [prf, in mathcomp.algebra.ring_tactic]
Internals.PevalM [prf, in mathcomp.algebra.ring_tactic]
Internals.PevalMC [prf, in mathcomp.algebra.ring_tactic]
Internals.PevalN [prf, in mathcomp.algebra.ring_tactic]
Internals.PExpr_eqP [prf, in mathcomp.algebra.field_tactic]
Internals.PExpr_R_eq [prf, in mathcomp.algebra.field_tactic]
Internals.PExpr_R_map [prf, in mathcomp.algebra.ring_tactic]
Internals.PExpr_R_PEmap2 [prf, in mathcomp.algebra.field_tactic]
Internals.Pol_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Popp_id [prf, in mathcomp.algebra.ring_tactic]
Internals.PosDA [prf, in mathcomp.algebra.ring_tactic]
Internals.positive_R_eq [prf, in mathcomp.algebra.ring_tactic]
Internals.positive_Rxx [prf, in mathcomp.algebra.ring_tactic]
Internals.PosMC [prf, in mathcomp.algebra.ring_tactic]
Internals.PosSD [prf, in mathcomp.algebra.ring_tactic]
Internals.Psatz_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Psub_add [prf, in mathcomp.algebra.ring_tactic]
Internals.PsubI_addI [prf, in mathcomp.algebra.ring_tactic]
Internals.PsubX_addX [prf, in mathcomp.algebra.ring_tactic]
Internals.QTautoCheckerT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.R_of_N_natmul [prf, in mathcomp.algebra.ring_tactic]
Internals.R_of_Q_ratr [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.R_of_Z_intr [prf, in mathcomp.algebra.ring_tactic]
Internals.RBFeval_map_AC_of_C [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.RBFeval_map_AC_of_C_bool [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.RFevalP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.ring_checker_map_int_of_Z [prf, in mathcomp.algebra.ring_tactic]
Internals.ring_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.Rnorm_bf_correct [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Rnorm_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.Rnorm_eq_F_of_N [prf, in mathcomp.algebra.ring_tactic]
Internals.Rnorm_formula_correct [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.RTautoChecker_sound [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.sCring_checkerT [prf, in mathcomp.algebra.ring_tactic]
Internals.semiring_checker_map_N_to_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.semiring_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.sMeval_mk_monpol_list [prf, in mathcomp.algebra.ring_tactic]
Internals.sPEeval_eqs_PEeval [prf, in mathcomp.algebra.ring_tactic]
Internals.sPeval_norm_subst [prf, in mathcomp.algebra.ring_tactic]
Internals.sPeval_Pol_of_PExpr [prf, in mathcomp.algebra.ring_tactic]
Internals.split_neq0_l [prf, in mathcomp.algebra.field_tactic]
Internals.split_neq0_r [prf, in mathcomp.algebra.field_tactic]
Internals.tauto_checkerT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.uint_N_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.unit_Rxx [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Zfield_correct [prf, in mathcomp.algebra.field_tactic]
Internals.Zint_pow_pos_pos [prf, in mathcomp.algebra.field_tactic]
Internals.ZnumField_correct [prf, in mathcomp.algebra.field_tactic]
Internals.Zring_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.ZTautoCheckerT [prf, in mathcomp.algebra.arithmetic_tactic]
interval_display [prf, in mathcomp.algebra.interval]
IntervalCan.interval_can [prf, in mathcomp.algebra.interval]
IntervalCan.itv_bound_can [prf, in mathcomp.algebra.interval]
intEsg [prf, in mathcomp.algebra.ssrint]
intEsign [prf, in mathcomp.algebra.ssrint]
IntItv.mul_boundr_gt0 [prf, in mathcomp.algebra.interval_inference]
IntItv.mul_boundrC [prf, in mathcomp.algebra.interval_inference]
IntItv.opp_bound_ge0 [prf, in mathcomp.algebra.interval_inference]
IntItv.opp_bound_gt0 [prf, in mathcomp.algebra.interval_inference]
intmul1_is_monoid_morphism [prf, in mathcomp.algebra.ssrint]
intOrdered.gez0_norm [prf, in mathcomp.algebra.ssrint]
intOrdered.lez_add [prf, in mathcomp.algebra.ssrint]
intOrdered.lez_anti [prf, in mathcomp.algebra.ssrint]
intOrdered.lez_mul [prf, in mathcomp.algebra.ssrint]
intOrdered.lez_total [prf, in mathcomp.algebra.ssrint]
intOrdered.ltz_def [prf, in mathcomp.algebra.ssrint]
intOrdered.normzN [prf, in mathcomp.algebra.ssrint]
intOrdered.subz_ge0 [prf, in mathcomp.algebra.ssrint]
intP [prf, in mathcomp.algebra.ssrint]
intq_eq0 [prf, in mathcomp.algebra.rat]
intr1D [prf, in mathcomp.algebra.ssrint]
intr_eq0 [prf, in mathcomp.algebra.ssrint]
intr_norm [prf, in mathcomp.algebra.ssrint]
intr_pos_nat_neq0 [prf, in mathcomp.algebra.binnums]
intr_sg [prf, in mathcomp.algebra.ssrint]
intr_sign [prf, in mathcomp.algebra.ssrint]
intrB [prf, in mathcomp.algebra.ssrint]
intrD [prf, in mathcomp.algebra.ssrint]
intrD1 [prf, in mathcomp.algebra.ssrint]
intRing.mul0z [prf, in mathcomp.algebra.ssrint]
intRing.mul1z [prf, in mathcomp.algebra.ssrint]
intRing.mulNz [prf, in mathcomp.algebra.ssrint]
intRing.mulz0 [prf, in mathcomp.algebra.ssrint]
intRing.mulz_addl [prf, in mathcomp.algebra.ssrint]
intRing.mulzA [prf, in mathcomp.algebra.ssrint]
intRing.mulzC [prf, in mathcomp.algebra.ssrint]
intRing.mulzN [prf, in mathcomp.algebra.ssrint]
intRing.mulzS [prf, in mathcomp.algebra.ssrint]
intRing.nonzero1z [prf, in mathcomp.algebra.ssrint]
intrM [prf, in mathcomp.algebra.ssrint]
intrN [prf, in mathcomp.algebra.ssrint]
intro_adjunction [prf, in mathcomp.boot.fingraph]
intro_class_fun [prf, in mathcomp.group_representation.classfun]
intro_closed [prf, in mathcomp.boot.fingraph]
intro_isoGrp [prf, in mathcomp.finite_group.presentation]
intro_mxsemisimple [prf, in mathcomp.group_representation.mxrepresentation]
intro_unitmx [prf, in mathcomp.algebra.matrix]
intrV [prf, in mathcomp.algebra.ssrint]
intS [prf, in mathcomp.algebra.ssrint]
intUnitRing.idomain_axiomz [prf, in mathcomp.algebra.ssrint]
intUnitRing.invz_out [prf, in mathcomp.algebra.ssrint]
intUnitRing.mulVz [prf, in mathcomp.algebra.ssrint]
intUnitRing.mulzn_eq1 [prf, in mathcomp.algebra.ssrint]
intUnitRing.unitzPl [prf, in mathcomp.algebra.ssrint]
intz [prf, in mathcomp.algebra.ssrint]
intZmod.add0z [prf, in mathcomp.algebra.ssrint]
intZmod.add1Pz [prf, in mathcomp.algebra.ssrint]
intZmod.addNz [prf, in mathcomp.algebra.ssrint]
intZmod.addPz [prf, in mathcomp.algebra.ssrint]
intZmod.addSnz [prf, in mathcomp.algebra.ssrint]
intZmod.addSz [prf, in mathcomp.algebra.ssrint]
intZmod.addzA [prf, in mathcomp.algebra.ssrint]
intZmod.addzC [prf, in mathcomp.algebra.ssrint]
intZmod.int_rect [prf, in mathcomp.algebra.ssrint]
intZmod.intP [prf, in mathcomp.algebra.ssrint]
intZmod.NegzE [prf, in mathcomp.algebra.ssrint]
intZmod.oppzD [prf, in mathcomp.algebra.ssrint]
intZmod.oppzK [prf, in mathcomp.algebra.ssrint]
intZmod.PoszD [prf, in mathcomp.algebra.ssrint]
intZmod.predn_int [prf, in mathcomp.algebra.ssrint]
intZmod.subSz1 [prf, in mathcomp.algebra.ssrint]
inv_dprod_Iirr0 [prf, in mathcomp.group_representation.character]
inv_dprod_IirrK [prf, in mathcomp.group_representation.character]
inv_eq [prf, in mathcomp.boot.eqtype]
inv_is_ahom [prf, in mathcomp.field.galois]
inv_kHomf [prf, in mathcomp.field.galois]
inv_lfun_def [prf, in mathcomp.algebra.vector]
inv_quotientN [prf, in mathcomp.finite_group.quotient]
inv_quotientS [prf, in mathcomp.finite_group.quotient]
inv_subG [prf, in mathcomp.finite_group.fingroup]
invariant_chief_irr_cases [prf, in mathcomp.group_representation.inertia]
invariant_comp [prf, in mathcomp.boot.eqtype]
invariant_inj [prf, in mathcomp.boot.eqtype]
invariant_subnormal [prf, in mathcomp.solvable.gseries]
invb_out [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
invCg [prf, in mathcomp.finite_group.fingroup]
invDg [prf, in mathcomp.finite_group.fingroup]
invF_f [prf, in mathcomp.boot.fintype]
invg1 [prf, in mathcomp.boot.monoid]
invg2id [prf, in mathcomp.finite_group.fingroup]
invg_eq1 [prf, in mathcomp.boot.monoid]
invg_expg [prf, in mathcomp.finite_group.fingroup]
invg_ffun [prf, in mathcomp.finite_group.gproduct]
invg_inj [prf, in mathcomp.boot.monoid]
invg_lcoset [prf, in mathcomp.finite_group.fingroup]
invg_lcosets [prf, in mathcomp.finite_group.fingroup]
invg_rcoset [prf, in mathcomp.finite_group.fingroup]
invg_set1 [prf, in mathcomp.finite_group.fingroup]
invgF [prf, in mathcomp.boot.monoid]
invGid [prf, in mathcomp.finite_group.fingroup]
invgR [prf, in mathcomp.boot.monoid]
invIg [prf, in mathcomp.finite_group.fingroup]
invm_subker [prf, in mathcomp.finite_group.morphism]
invmE [prf, in mathcomp.finite_group.morphism]
invMG [prf, in mathcomp.finite_group.fingroup]
invmK [prf, in mathcomp.finite_group.morphism]
invmx1 [prf, in mathcomp.algebra.matrix]
invmx_block_diag [prf, in mathcomp.algebra.matrix]
invmx_out [prf, in mathcomp.algebra.matrix]
invmx_scalar [prf, in mathcomp.algebra.matrix]
invmx_unitary [prf, in mathcomp.algebra.spectral]
invmxK [prf, in mathcomp.algebra.matrix]
invmxZ [prf, in mathcomp.algebra.matrix]
involutions_gen_dihedral [prf, in mathcomp.solvable.extremal]
invq0 [prf, in mathcomp.algebra.rat]
invq_def [prf, in mathcomp.algebra.rat]
invq_frac [prf, in mathcomp.algebra.rat]
invr_expz [prf, in mathcomp.algebra.ssrint]
invr_lin_char [prf, in mathcomp.group_representation.character]
invSg [prf, in mathcomp.finite_group.fingroup]
invUg [prf, in mathcomp.finite_group.fingroup]
iota_ltn_sorted [prf, in mathcomp.boot.path]
iota_sorted [prf, in mathcomp.boot.path]
iota_tupleP [prf, in mathcomp.boot.tuple]
iota_uniq [prf, in mathcomp.boot.seq]
iotaD [prf, in mathcomp.boot.seq]
iotaDl [prf, in mathcomp.boot.seq]
irr0 [prf, in mathcomp.group_representation.character]
irr1_abelian_bound [prf, in mathcomp.group_representation.character]
irr1_bound [prf, in mathcomp.group_representation.character]
irr1_degree [prf, in mathcomp.group_representation.character]
irr1_gt0 [prf, in mathcomp.group_representation.character]
irr1_mode [prf, in mathcomp.group_representation.mxrepresentation]
irr1_neq0 [prf, in mathcomp.group_representation.character]
irr1_repr [prf, in mathcomp.group_representation.mxrepresentation]
irr1_rfix [prf, in mathcomp.group_representation.mxrepresentation]
irr_aut_closed [prf, in mathcomp.group_representation.character]
irr_basis [prf, in mathcomp.group_representation.character]
irr_center_scalar [prf, in mathcomp.group_representation.mxrepresentation]
irr_cfcenterE [prf, in mathcomp.group_representation.character]
irr_char [prf, in mathcomp.group_representation.character]
irr_classK [prf, in mathcomp.group_representation.character]
irr_classP [prf, in mathcomp.group_representation.character]
irr_comp'_op0_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_comp_envelop_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_comp_id_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_comp_rsim_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_constt_to_dirr [prf, in mathcomp.group_representation.vcharacter]
irr_consttE [prf, in mathcomp.group_representation.character]
irr_cyclic_lin [prf, in mathcomp.group_representation.character]
irr_degree_abelian [prf, in mathcomp.group_representation.mxrepresentation]
irr_degree_gt0 [prf, in mathcomp.group_representation.mxrepresentation]
irr_degreeE [prf, in mathcomp.group_representation.mxrepresentation]
irr_dirr [prf, in mathcomp.group_representation.vcharacter]
irr_eq1 [prf, in mathcomp.group_representation.character]
irr_faithful_center [prf, in mathcomp.group_representation.character]
irr_free [prf, in mathcomp.group_representation.character]
irr_gring_center [prf, in mathcomp.group_representation.integral_char]
irr_induced_Frobenius_ker [prf, in mathcomp.group_representation.inertia]
irr_inj [prf, in mathcomp.group_representation.character]
irr_inv [prf, in mathcomp.group_representation.character]
irr_mode1 [prf, in mathcomp.group_representation.mxrepresentation]
irr_mode_neq0 [prf, in mathcomp.group_representation.mxrepresentation]
irr_mode_unit [prf, in mathcomp.group_representation.mxrepresentation]
irr_modeM [prf, in mathcomp.group_representation.mxrepresentation]
irr_modeV [prf, in mathcomp.group_representation.mxrepresentation]
irr_modeX [prf, in mathcomp.group_representation.mxrepresentation]
irr_mx_mult_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_mx_sum_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_neq0 [prf, in mathcomp.group_representation.character]
irr_of_socle_bij [prf, in mathcomp.group_representation.character]
irr_of_socleK [prf, in mathcomp.group_representation.character]
irr_orthonormal [prf, in mathcomp.group_representation.character]
irr_prime_injP [prf, in mathcomp.group_representation.character]
irr_prime_lin [prf, in mathcomp.group_representation.character]
irr_repr'_op0_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_repr_lin_char [prf, in mathcomp.group_representation.character]
irr_reprE [prf, in mathcomp.group_representation.mxrepresentation]
irr_reprK_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_reprP [prf, in mathcomp.group_representation.character]
irr_sorted_eq [prf, in mathcomp.boot.path]
irr_sorted_eq_in [prf, in mathcomp.boot.path]
irr_sum_square [prf, in mathcomp.group_representation.character]
irr_vchar [prf, in mathcomp.group_representation.vcharacter]
irr_vchar_on [prf, in mathcomp.group_representation.vcharacter]
irrEchar [prf, in mathcomp.group_representation.character]
irredp_FAdjoin [prf, in mathcomp.field.fieldext]
irreducible_poly_coprime [prf, in mathcomp.algebra.qpoly]
irreducible_rat_int [prf, in mathcomp.algebra.rat]
irreducibleP [prf, in mathcomp.algebra.qpoly]
irrK [prf, in mathcomp.group_representation.character]
irrP [prf, in mathcomp.group_representation.character]
irrRepr [prf, in mathcomp.group_representation.character]
irrWchar [prf, in mathcomp.group_representation.character]
irrWnorm [prf, in mathcomp.group_representation.character]
is_abelem_pgroup [prf, in mathcomp.solvable.abelian]
is_abelemP [prf, in mathcomp.solvable.abelian]
is_diag_block_mx [prf, in mathcomp.algebra.matrix]
is_diag_mx_is_trig [prf, in mathcomp.algebra.matrix]
is_diag_mxblock [prf, in mathcomp.algebra.matrix]
is_diag_mxblockP [prf, in mathcomp.algebra.matrix]
is_diag_mxEtrig [prf, in mathcomp.algebra.matrix]
is_diag_mxP [prf, in mathcomp.algebra.matrix]
is_diag_trmx [prf, in mathcomp.algebra.matrix]
is_hermitianmxE [prf, in mathcomp.algebra.sesquilinear]
is_hermitianmxP [prf, in mathcomp.algebra.sesquilinear]
is_iso3P [prf, in mathcomp.solvable.burnside_app]
is_isoP [prf, in mathcomp.solvable.burnside_app]
is_perm_mx1 [prf, in mathcomp.algebra.matrix]
is_perm_mx_tr [prf, in mathcomp.algebra.matrix]
is_perm_mxMl [prf, in mathcomp.algebra.matrix]
is_perm_mxMr [prf, in mathcomp.algebra.matrix]
is_perm_mxP [prf, in mathcomp.algebra.matrix]
is_perm_mxV [prf, in mathcomp.algebra.matrix]
is_scalar_mx_is_diag [prf, in mathcomp.algebra.matrix]
is_scalar_mx_is_trig [prf, in mathcomp.algebra.matrix]
is_scalar_mxP [prf, in mathcomp.algebra.matrix]
is_total_action [prf, in mathcomp.finite_group.action]
is_trig_block_mx [prf, in mathcomp.algebra.matrix]
is_trig_mxblock [prf, in mathcomp.algebra.matrix]
is_trig_mxblockP [prf, in mathcomp.algebra.matrix]
is_trig_mxP [prf, in mathcomp.algebra.matrix]
isgroupP [prf, in mathcomp.finite_group.fingroup]
iso0_1 [prf, in mathcomp.solvable.burnside_app]
iso3_ndir [prf, in mathcomp.solvable.burnside_app]
iso_eq_F0_F1 [prf, in mathcomp.solvable.burnside_app]
iso_eq_F0_F1_F2 [prf, in mathcomp.solvable.burnside_app]
isog_2extraspecial [prf, in mathcomp.solvable.extraspecial]
isog_2X1p2 [prf, in mathcomp.solvable.extraspecial]
isog_abelem [prf, in mathcomp.solvable.abelian]
isog_abelem_card [prf, in mathcomp.solvable.abelian]
isog_abelem_rV [prf, in mathcomp.group_representation.mxabelem]
isog_abelian [prf, in mathcomp.finite_group.morphism]
isog_abelian_type [prf, in mathcomp.solvable.abelian]
isog_center [prf, in mathcomp.solvable.center]
isog_cprod_by [prf, in mathcomp.solvable.center]
isog_cyclic [prf, in mathcomp.solvable.cyclic]
isog_cyclic_card [prf, in mathcomp.solvable.cyclic]
isog_der [prf, in mathcomp.solvable.commutator]
isog_dprod [prf, in mathcomp.finite_group.gproduct]
isog_eq1 [prf, in mathcomp.finite_group.morphism]
isog_extraspecial [prf, in mathcomp.solvable.maximal]
isog_Fitting [prf, in mathcomp.solvable.maximal]
isog_grank [prf, in mathcomp.solvable.abelian]
isog_hom [prf, in mathcomp.finite_group.morphism]
isog_homocyclic [prf, in mathcomp.solvable.abelian]
isog_isom [prf, in mathcomp.finite_group.morphism]
isog_Mho [prf, in mathcomp.solvable.abelian]
isog_nil [prf, in mathcomp.solvable.nilpotent]
isog_nil_class [prf, in mathcomp.solvable.nilpotent]
isog_Ohm [prf, in mathcomp.solvable.abelian]
isog_p_rank [prf, in mathcomp.solvable.abelian]
isog_pcore [prf, in mathcomp.solvable.pgroup]
isog_pgroup [prf, in mathcomp.solvable.pgroup]
isog_Phi [prf, in mathcomp.solvable.maximal]
isog_pseries [prf, in mathcomp.solvable.pgroup]
isog_pX1p2 [prf, in mathcomp.solvable.extraspecial]
isog_pX1p2n [prf, in mathcomp.solvable.extraspecial]
isog_rank [prf, in mathcomp.solvable.abelian]
isog_refl [prf, in mathcomp.finite_group.morphism]
isog_set1X [prf, in mathcomp.finite_group.gproduct]
isog_setX1 [prf, in mathcomp.finite_group.gproduct]
isog_setXn [prf, in mathcomp.finite_group.gproduct]
isog_simple [prf, in mathcomp.solvable.gseries]
isog_sol [prf, in mathcomp.solvable.nilpotent]
isog_special [prf, in mathcomp.solvable.maximal]
isog_subg [prf, in mathcomp.finite_group.morphism]
isog_sym [prf, in mathcomp.finite_group.morphism]
isog_symr [prf, in mathcomp.finite_group.morphism]
isog_trans [prf, in mathcomp.finite_group.morphism]
isog_transl [prf, in mathcomp.finite_group.morphism]
isog_transr [prf, in mathcomp.finite_group.morphism]
isog_xcprod [prf, in mathcomp.solvable.center]
isogEcard [prf, in mathcomp.finite_group.morphism]
isogEhom [prf, in mathcomp.finite_group.morphism]
isogP [prf, in mathcomp.finite_group.morphism]
isoGrp_hom [prf, in mathcomp.finite_group.presentation]
isoGrp_trans [prf, in mathcomp.finite_group.presentation]
isoGrpP [prf, in mathcomp.finite_group.presentation]
isom_card [prf, in mathcomp.finite_group.morphism]
isom_cast_perm [prf, in mathcomp.finite_group.perm]
isom_Iirr0 [prf, in mathcomp.group_representation.character]
isom_Iirr_eq0 [prf, in mathcomp.group_representation.character]
isom_Iirr_inj [prf, in mathcomp.group_representation.character]
isom_IirrE [prf, in mathcomp.group_representation.character]
isom_IirrK [prf, in mathcomp.group_representation.character]
isom_IirrKV [prf, in mathcomp.group_representation.character]
isom_im [prf, in mathcomp.finite_group.morphism]
isom_inj [prf, in mathcomp.finite_group.morphism]
isom_isog [prf, in mathcomp.finite_group.morphism]
isom_restr_perm [prf, in mathcomp.finite_group.action]
isom_sgval [prf, in mathcomp.finite_group.morphism]
isom_sub_im [prf, in mathcomp.finite_group.morphism]
isom_subg [prf, in mathcomp.finite_group.morphism]
isom_sym [prf, in mathcomp.finite_group.morphism]
isometries_iso [prf, in mathcomp.solvable.burnside_app]
isometry_in_zchar [prf, in mathcomp.group_representation.vcharacter]
isometry_of_cfnorm [prf, in mathcomp.group_representation.classfun]
isometry_of_dnorm [prf, in mathcomp.algebra.sesquilinear]
isometry_of_free [prf, in mathcomp.group_representation.classfun]
isometry_of_free [prf, in mathcomp.algebra.sesquilinear]
isometry_raddf_inj [prf, in mathcomp.group_representation.classfun]
isometry_raddf_inj [prf, in mathcomp.algebra.sesquilinear]
isomP [prf, in mathcomp.finite_group.morphism]
isSome_insub [prf, in mathcomp.boot.eqtype]
iter_addn [prf, in mathcomp.boot.ssrnat]
iter_addn_0 [prf, in mathcomp.boot.ssrnat]
iter_findex [prf, in mathcomp.boot.fingraph]
iter_finv [prf, in mathcomp.boot.fingraph]
iter_finv_cycle [prf, in mathcomp.boot.fingraph]
iter_finv_in [prf, in mathcomp.boot.fingraph]
iter_fix [prf, in mathcomp.boot.ssrnat]
iter_in [prf, in mathcomp.boot.ssrnat]
iter_mulg [prf, in mathcomp.boot.monoid]
iter_mulg_1 [prf, in mathcomp.boot.monoid]
iter_muln [prf, in mathcomp.boot.ssrnat]
iter_muln_1 [prf, in mathcomp.boot.ssrnat]
iter_opD2 [prf, in mathcomp.algebra.binnums]
iter_opDdoubler [prf, in mathcomp.algebra.binnums]
iter_order [prf, in mathcomp.boot.fingraph]
iter_order_cycle [prf, in mathcomp.boot.fingraph]
iter_order_in [prf, in mathcomp.boot.fingraph]
iter_porbit [prf, in mathcomp.finite_group.perm]
iter_predn [prf, in mathcomp.boot.ssrnat]
iter_sub_fix [prf, in mathcomp.boot.finset]
iter_succn [prf, in mathcomp.boot.ssrnat]
iter_succn_0 [prf, in mathcomp.boot.ssrnat]
iterD [prf, in mathcomp.boot.ssrnat]
iteriS [prf, in mathcomp.boot.ssrnat]
iterM [prf, in mathcomp.boot.ssrnat]
iteropS [prf, in mathcomp.boot.ssrnat]
iterS [prf, in mathcomp.boot.ssrnat]
iterSr [prf, in mathcomp.boot.ssrnat]
iterX [prf, in mathcomp.boot.ssrnat]
Itv.spec_real1 [prf, in mathcomp.algebra.interval_inference]
Itv.spec_real2 [prf, in mathcomp.algebra.interval_inference]
itv01_subdef [prf, in mathcomp.algebra.interval_inference]
itv_bound_display [prf, in mathcomp.algebra.interval]
itv_bound_total [prf, in mathcomp.algebra.interval]
itv_boundlr [prf, in mathcomp.algebra.interval]
itv_dec [prf, in mathcomp.algebra.interval]
itv_ge [prf, in mathcomp.algebra.interval]
itv_joinA [prf, in mathcomp.algebra.interval]
itv_joinC [prf, in mathcomp.algebra.interval]
itv_joinKI [prf, in mathcomp.algebra.interval]
itv_le0x [prf, in mathcomp.algebra.interval]
itv_leEmeet [prf, in mathcomp.algebra.interval]
itv_lex1 [prf, in mathcomp.algebra.interval]
itv_meetA [prf, in mathcomp.algebra.interval]
itv_meetC [prf, in mathcomp.algebra.interval]
itv_meetKU [prf, in mathcomp.algebra.interval]
itv_meetUl [prf, in mathcomp.algebra.interval]
itv_split1U [prf, in mathcomp.algebra.interval]
itv_splitI [prf, in mathcomp.algebra.interval]
itv_splitU [prf, in mathcomp.algebra.interval]
itv_splitU1 [prf, in mathcomp.algebra.interval]
itv_splitUeq [prf, in mathcomp.algebra.interval]
itv_total_join3E [prf, in mathcomp.algebra.interval]
itv_total_meet3E [prf, in mathcomp.algebra.interval]
itv_xx [prf, in mathcomp.algebra.interval]
itvnum_subdef [prf, in mathcomp.algebra.interval_inference]
itvP [prf, in mathcomp.algebra.interval]
itvreal_subdef [prf, in mathcomp.algebra.interval_inference]
itvxx [prf, in mathcomp.algebra.interval]
itvxxP [prf, in mathcomp.algebra.interval]