I (Global Index)
| 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
I [abbrev, in mathcomp.algebra.ring_quotient]I [abbrev, in mathcomp.algebra.ring_quotient]
iC [abbrev, in mathcomp.group_representation.character]
id1 [def, in mathcomp.solvable.burnside_app]
id3 [def, in mathcomp.solvable.burnside_app]
id_ahom [def, in mathcomp.field.falgebra]
id_is_ahom [prf, in mathcomp.field.falgebra]
id_lfun [def, in mathcomp.algebra.vector]
id_lfunE [prf, in mathcomp.algebra.vector]
idealMr [prf, in mathcomp.algebra.ring_quotient]
Idealr [abbrev, in mathcomp.algebra.ring_quotient]
Idealr [mod, in mathcomp.algebra.ring_quotient]
Idealr.Algebra_isAddClosed_mixin [proj, in mathcomp.algebra.ring_quotient]
Idealr.Algebra_isOppClosed_mixin [proj, in mathcomp.algebra.ring_quotient]
Idealr.axioms_ [rec, in mathcomp.algebra.ring_quotient]
Idealr.class [proj, in mathcomp.algebra.ring_quotient]
Idealr.clone [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.copy [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.Exports [mod, in mathcomp.algebra.ring_quotient]
Idealr.Exports.idealr [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.Exports.join_ring_quotient_Idealr_between_Algebra_AddClosed_and_ring_quotient_ProperIdeal [def, in mathcomp.algebra.ring_quotient]
Idealr.Exports.join_ring_quotient_Idealr_between_Algebra_OppClosed_and_ring_quotient_ProperIdeal [def, in mathcomp.algebra.ring_quotient]
Idealr.Exports.join_ring_quotient_Idealr_between_ring_quotient_ProperIdeal_and_Algebra_ZmodClosed [def, in mathcomp.algebra.ring_quotient]
Idealr.on [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.on_ [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.pack_ [def, in mathcomp.algebra.ring_quotient]
Idealr.phant_clone [def, in mathcomp.algebra.ring_quotient]
Idealr.phant_on_ [def, in mathcomp.algebra.ring_quotient]
Idealr.ring_quotient_isProperIdeal_mixin [proj, in mathcomp.algebra.ring_quotient]
Idealr.sort [proj, in mathcomp.algebra.ring_quotient]
Idealr.type [rec, in mathcomp.algebra.ring_quotient]
idealr0 [prf, in mathcomp.algebra.ring_quotient]
idealr1 [prf, in mathcomp.algebra.ring_quotient]
idealr_closed [def, in mathcomp.algebra.ring_quotient]
idealr_closed_nontrivial [prf, in mathcomp.algebra.ring_quotient]
idealr_closedB [prf, in mathcomp.algebra.ring_quotient]
IdealrElpiOperations [mod, in mathcomp.algebra.ring_quotient]
idem_sub_le_big [prf, in mathcomp.boot.bigop]
idem_sub_le_big_cond [prf, in mathcomp.boot.bigop]
idempotent [abbrev, in mathcomp.boot.ssrfun]
idempotent_fun [def, in mathcomp.boot.ssrfun]
idempotent_op [def, in mathcomp.boot.ssrfun]
idfun_gmulf1 [prf, in mathcomp.boot.monoid]
idfun_gmulfM [prf, in mathcomp.boot.monoid]
idGfun [def, in mathcomp.solvable.gfunctor]
idGfun_closed [prf, in mathcomp.solvable.gfunctor]
idGfun_cont [prf, in mathcomp.solvable.gfunctor]
idGfun_monotonic [prf, in mathcomp.solvable.gfunctor]
idm [def, in mathcomp.finite_group.morphism]
idm_isom [prf, in mathcomp.finite_group.morphism]
idm_morphism [def, in mathcomp.finite_group.morphism]
idm_morphM [prf, in mathcomp.finite_group.morphism]
idmxE [prf, in mathcomp.algebra.matrix]
Idummy_placeholder [ind, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
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]
ifactm [def, in mathcomp.finite_group.morphism]
ifactmE [prf, in mathcomp.finite_group.morphism]
ifN_eq [prf, in mathcomp.boot.eqtype]
ifN_eqC [prf, in mathcomp.boot.eqtype]
iG [abbrev, in mathcomp.group_representation.mxrepresentation]
iinv [def, in mathcomp.boot.fintype]
iinv_f [prf, in mathcomp.boot.fintype]
iinv_proof [prf, in mathcomp.boot.fintype]
Iirr [abbrev, in mathcomp.group_representation.character]
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 [abbrev, in mathcomp.boot.fintype]
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_mem [def, 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]
image_tuple [def, in mathcomp.boot.tuple]
imageP [prf, in mathcomp.boot.fintype]
Immx_rect [prf, in mathcomp.algebra.spectral]
imprimitivity_system [def, in mathcomp.solvable.primitive_action]
imset [abbrev, in mathcomp.boot.finset]
imset [mod, in mathcomp.boot.finset]
imset.body [def, in mathcomp.boot.finset]
imset.unlock [def, in mathcomp.boot.finset]
imset0 [prf, in mathcomp.boot.finset]
imset0mem [prf, in mathcomp.boot.finset]
imset2 [abbrev, in mathcomp.boot.finset]
imset2 [mod, in mathcomp.boot.finset]
imset2.body [def, in mathcomp.boot.finset]
imset2.unlock [def, in mathcomp.boot.finset]
imset2_f [prf, in mathcomp.boot.finset]
imset2_Locked [modtype, in mathcomp.boot.finset]
imset2_Locked.body [ax, in mathcomp.boot.finset]
imset2_Locked.unlock [ax, 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]
imset2_spec [ind, in mathcomp.boot.finset]
imset2_unlock [def, in mathcomp.boot.finset]
imset2_unlock_subterm [def, in mathcomp.boot.finset]
imset2P [prf, in mathcomp.boot.finset]
imset2S [prf, in mathcomp.boot.finset]
imset2Sl [prf, in mathcomp.boot.finset]
Imset2spec [constr, 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_Locked [modtype, in mathcomp.boot.finset]
imset_Locked.body [ax, in mathcomp.boot.finset]
imset_Locked.unlock [ax, 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]
imset_unlock [def, in mathcomp.boot.finset]
imset_unlock_subterm [def, 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_bseq [def, in mathcomp.boot.tuple]
in_bseqE [prf, in mathcomp.boot.tuple]
in_cons [prf, in mathcomp.boot.seq]
in_cprod [def, in mathcomp.solvable.center]
in_cprod_morphism [def, in mathcomp.solvable.center]
in_cprodM [prf, in mathcomp.solvable.center]
in_Crat_span [def, in mathcomp.field.algnum]
in_factmod [def, in mathcomp.group_representation.mxrepresentation]
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_group [def, in mathcomp.finite_group.fingroup]
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_qpoly [def, in mathcomp.algebra.qpoly]
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_is_multiplicative [def, 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_sub_seq [abbrev, in mathcomp.boot.fintype]
in_submod [def, in mathcomp.group_representation.mxrepresentation]
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 [def, in mathcomp.boot.tuple]
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]
inA [abbrev, in mathcomp.solvable.hall]
INatmul [constr, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Inatmul [ind, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Inatmul_ind [scheme, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Inatmul_rec [scheme, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Inatmul_rect [scheme, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Inatmul_sind [scheme, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
incn_inj [prf, in mathcomp.boot.ssrnat]
incn_inj_in [prf, in mathcomp.boot.ssrnat]
incr_nth [def, in mathcomp.boot.seq]
incr_nth_inj [prf, in mathcomp.boot.seq]
incr_nthC [prf, in mathcomp.boot.seq]
incr_tally [def, in mathcomp.boot.seq]
incr_tallyP [prf, in mathcomp.boot.seq]
Ind_Iirr [def, in mathcomp.group_representation.character]
Ind_irr_neq0 [prf, in mathcomp.group_representation.character]
index [def, in mathcomp.boot.seq]
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 [def, in mathcomp.boot.bigop]
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_extremal_group_type [def, in mathcomp.solvable.extremal]
index_head [prf, in mathcomp.boot.seq]
index_inj [prf, in mathcomp.boot.seq]
index_injm [prf, in mathcomp.finite_group.quotient]
index_iota [def, in mathcomp.boot.bigop]
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]
indexg [def, in mathcomp.finite_group.fingroup]
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]
indir_iso3l [def, in mathcomp.solvable.burnside_app]
inE [def, in mathcomp.finite_group.fingroup]
inE [def, in mathcomp.boot.seq]
inE [def, in mathcomp.boot.finset]
inertia [file, in mathcomp.group_representation.inertia]
inertia [def, in mathcomp.group_representation.inertia]
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_group [def, 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]
infE [abbrev, in mathcomp.solvable.burnside_app]
infH [abbrev, in mathcomp.finite_group.action]
infix [def, in mathcomp.boot.seq]
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_index [def, 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]
inG [abbrev, in mathcomp.solvable.hall]
inH [abbrev, in mathcomp.finite_group.action]
inIntSpan [def, in mathcomp.algebra.rat]
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_subfx [def, in mathcomp.field.fieldext]
inj_tperm [prf, in mathcomp.finite_group.perm]
inj_type [def, in mathcomp.boot.eqtype]
injective2 [def, in mathcomp.boot.ssrfun]
injectiveb [def, in mathcomp.boot.fintype]
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]
inlined_new_rect [abbrev, in mathcomp.boot.eqtype]
inlined_sub_rect [abbrev, in mathcomp.boot.eqtype]
innew [def, in mathcomp.boot.eqtype]
innew_val [prf, in mathcomp.boot.eqtype]
inord [def, in mathcomp.boot.fintype]
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]
insigd [def, in mathcomp.boot.eqtype]
Instances [mod, in mathcomp.algebra.interval_inference]
Instances.add_inum [def, in mathcomp.algebra.interval_inference]
Instances.addn_inum [def, in mathcomp.algebra.interval_inference]
Instances.BRight_le_mul_boundr [prf, in mathcomp.algebra.interval_inference]
Instances.comparable_num_itv_bound [prf, in mathcomp.algebra.interval_inference]
Instances.double_inum [def, in mathcomp.algebra.interval_inference]
Instances.expn_inum [def, in mathcomp.algebra.interval_inference]
Instances.exprn_inum [def, in mathcomp.algebra.interval_inference]
Instances.exprz_inum [def, in mathcomp.algebra.interval_inference]
Instances.factorial_inum [def, in mathcomp.algebra.interval_inference]
Instances.intmul_inum [def, in mathcomp.algebra.interval_inference]
Instances.inv_inum [def, in mathcomp.algebra.interval_inference]
Instances.ISignBoth [constr, in mathcomp.algebra.interval_inference]
Instances.ISignEqZero [constr, in mathcomp.algebra.interval_inference]
Instances.ISignNonNeg [constr, in mathcomp.algebra.interval_inference]
Instances.ISignNonPos [constr, in mathcomp.algebra.interval_inference]
Instances.max_typ_inum [def, in mathcomp.algebra.interval_inference]
Instances.maxn_inum [def, in mathcomp.algebra.interval_inference]
Instances.min_max_maxP [proj, in mathcomp.algebra.interval_inference]
Instances.min_max_minP [proj, in mathcomp.algebra.interval_inference]
Instances.min_max_sem [proj, in mathcomp.algebra.interval_inference]
Instances.min_max_sort [proj, in mathcomp.algebra.interval_inference]
Instances.min_max_typ [rec, in mathcomp.algebra.interval_inference]
Instances.min_typ_inum [def, in mathcomp.algebra.interval_inference]
Instances.minn_inum [def, in mathcomp.algebra.interval_inference]
Instances.mul_inum [def, in mathcomp.algebra.interval_inference]
Instances.muln_inum [def, in mathcomp.algebra.interval_inference]
Instances.nat_min_max_typ [def, 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.natmul_inum [def, in mathcomp.algebra.interval_inference]
Instances.natmul_itv [def, in mathcomp.algebra.interval_inference]
Instances.Negz_inum [def, in mathcomp.algebra.interval_inference]
Instances.norm_inum [def, 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_min_max_typ [def, 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.one_inum [def, in mathcomp.algebra.interval_inference]
Instances.opp_boundl [prf, in mathcomp.algebra.interval_inference]
Instances.opp_boundr [prf, in mathcomp.algebra.interval_inference]
Instances.opp_inum [def, in mathcomp.algebra.interval_inference]
Instances.Posz_inum [def, in mathcomp.algebra.interval_inference]
Instances.sign_spec [ind, in mathcomp.algebra.interval_inference]
Instances.signP [prf, in mathcomp.algebra.interval_inference]
Instances.sqrt_inum [def, in mathcomp.algebra.interval_inference]
Instances.sqrt_itv [def, in mathcomp.algebra.interval_inference]
Instances.sqrtC_inum [def, in mathcomp.algebra.interval_inference]
Instances.sqrtC_itv [def, in mathcomp.algebra.interval_inference]
Instances.succn_inum [def, in mathcomp.algebra.interval_inference]
Instances.zero_inum [def, in mathcomp.algebra.interval_inference]
Instances.zeron_inum [def, in mathcomp.algebra.interval_inference]
insub [def, in mathcomp.boot.eqtype]
insub_bseq [def, in mathcomp.boot.tuple]
insub_eq [def, in mathcomp.boot.eqtype]
insub_eqE [prf, in mathcomp.boot.eqtype]
insub_spec [ind, in mathcomp.boot.eqtype]
insubd [def, 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]
InsubNone [constr, in mathcomp.boot.eqtype]
insubP [prf, in mathcomp.boot.eqtype]
InsubSome [constr, in mathcomp.boot.eqtype]
insubT [prf, in mathcomp.boot.eqtype]
int [ind, in mathcomp.algebra.ssrint]
int_ind [def, in mathcomp.algebra.ssrint]
int_of_natsum [def, in mathcomp.algebra.ssrint]
int_of_Z [def, in mathcomp.algebra.binnums]
int_rec [def, in mathcomp.algebra.ssrint]
int_rect [prf, in mathcomp.algebra.ssrint]
int_Smith_normal_form [prf, in mathcomp.algebra.intdiv]
int_spec [ind, in mathcomp.algebra.ssrint]
intCK [abbrev, in mathcomp.field.cyclotomic]
IntDist [mod, in mathcomp.algebra.ssrint]
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.int_nmodType [def, in mathcomp.algebra.ssrint]
IntDist.int_zmodType [def, 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]
intdiv [file, in mathcomp.algebra.intdiv]
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_char [file, in mathcomp.group_representation.integral_char]
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]
integralOver [def, in mathcomp.algebra.mxpoly]
integralRange [def, in mathcomp.algebra.mxpoly]
Internals [mod, in mathcomp.algebra.ring_tactic]
Internals [mod, in mathcomp.algebra.field_tactic]
Internals [mod, in mathcomp.algebra.arithmetic_tactic]
Internals.A_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.absurd_PCond_R [def, in mathcomp.algebra.field_tactic]
Internals.add_pos_nat [def, in mathcomp.algebra.ring_tactic]
Internals.add_pos_natE [prf, in mathcomp.algebra.ring_tactic]
Internals.add_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.add_term [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.add_term_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.add_termP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.addb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.addf_div_common [prf, in mathcomp.algebra.field_tactic]
Internals.addn_expand [def, in mathcomp.algebra.ring_tactic]
Internals.and_cnf [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.and_cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.AND_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.and_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.andb_R [def, in mathcomp.algebra.ring_tactic]
Internals.app_R [def, in mathcomp.algebra.field_tactic]
Internals.apply_option_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.BFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.BFKFeval [def, in mathcomp.algebra.arithmetic_tactic]
Internals.BFKFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.BFormula_Q2Z [def, in mathcomp.algebra.arithmetic_tactic]
Internals.BFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.BFormula_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.bind_option2_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.bind_option_R [def, 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.Build_Formula_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.Ccnf_of_GFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.CFactor [abbrev, in mathcomp.algebra.ring_tactic]
Internals.CFactor_R [def, in mathcomp.algebra.ring_tactic]
Internals.Cfield_checkerT [prf, in mathcomp.algebra.field_tactic]
Internals.check_inconsistent [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.check_inconsistent_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.check_inconsistentT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.check_normalised_formulas [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.check_normalised_formulas [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.check_normalised_formulas_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.check_normalised_formulasT [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.check_normalised_formulasT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Cis_tauto_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.clause [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.clause_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cltb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cMeval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.cMeval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.cMeval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Cnegate_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cneqb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_checker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_ff [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_ff [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_ff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_negate [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_negate_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_normalise [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_normalise_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_of_GFormula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_of_GFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_of_list [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_of_list_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_tt [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_tt [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_tt_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Cnormalise_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.compare_cont_R [def, in mathcomp.algebra.ring_tactic]
Internals.compare_R [def, in mathcomp.algebra.ring_tactic]
Internals.cond_norm [abbrev, in mathcomp.algebra.field_tactic]
Internals.cond_norm [abbrev, in mathcomp.algebra.field_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.cond_norm_R [def, in mathcomp.algebra.field_tactic]
Internals.condition_R [def, in mathcomp.algebra.field_tactic]
Internals.conj_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.Cring_checkerT [prf, in mathcomp.algebra.ring_tactic]
Internals.CTautoChecker_map_AC_of_C [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.CTautoChecker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.CTautoCheckerT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Ctriv_divP [prf, in mathcomp.algebra.ring_tactic]
Internals.CWeakChecker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.deduce [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.default_isIn [abbrev, in mathcomp.algebra.field_tactic]
Internals.default_isIn_R [def, in mathcomp.algebra.field_tactic]
Internals.denum_R [def, in mathcomp.algebra.field_tactic]
Internals.double_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.double_pred_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.double_R [def, in mathcomp.algebra.ring_tactic]
Internals.eAND_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eFF_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eIFF_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eIMPL_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eKind_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eKind_Rxx [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eNOT_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.env_jump [def, in mathcomp.algebra.ring_tactic]
Internals.env_jumpD [prf, in mathcomp.algebra.ring_tactic]
Internals.env_nth [abbrev, in mathcomp.algebra.ring_tactic]
Internals.env_nth [abbrev, in mathcomp.algebra.ring_tactic]
Internals.env_nth [def, in mathcomp.algebra.ring_tactic]
Internals.env_nth [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.env_nth_jump [prf, in mathcomp.algebra.ring_tactic]
Internals.env_nth_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eOR_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eq_bool_R [prf, in mathcomp.algebra.ring_tactic]
Internals.eq_bool_R2 [prf, in mathcomp.algebra.ring_tactic]
Internals.EQ_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.eq_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.eq_refl_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.eq_Rnorm [prf, in mathcomp.algebra.ring_tactic]
Internals.eqb_R [def, in mathcomp.algebra.field_tactic]
Internals.eqb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eqb_R1 [def, in mathcomp.algebra.field_tactic]
Internals.Equal_R [constr, in mathcomp.algebra.arithmetic_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.eTT_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_and_cnf [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_clause [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_cnf [def, 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_op1 [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_op2_R [def, 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 [abbrev, 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_Psatz [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_Psatz_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_rev_append [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.expN [abbrev, in mathcomp.algebra.ring_tactic]
Internals.F_of_N [abbrev, in mathcomp.algebra.ring_tactic]
Internals.False_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.Fapp_R [def, in mathcomp.algebra.field_tactic]
Internals.Fcons0 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons00 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons00_R [def, in mathcomp.algebra.field_tactic]
Internals.Fcons0_R [def, in mathcomp.algebra.field_tactic]
Internals.Fcons1 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons1 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons1_R [def, in mathcomp.algebra.field_tactic]
Internals.Fcons2 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons2 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons2_R [def, in mathcomp.algebra.field_tactic]
Internals.FEadd_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEc_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEdiv_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEeval [abbrev, in mathcomp.algebra.field_tactic]
Internals.FEeval [abbrev, in mathcomp.algebra.field_tactic]
Internals.FEeval [abbrev, in mathcomp.algebra.field_tactic]
Internals.FEeval_map_int_of_Z [prf, in mathcomp.algebra.field_tactic]
Internals.FEI_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEinv_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEmul_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEO_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEopp_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEpow_R [constr, in mathcomp.algebra.field_tactic]
Internals.FEsub_R [constr, in mathcomp.algebra.field_tactic]
Internals.Feval [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.Feval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.FEX_R [constr, in mathcomp.algebra.field_tactic]
Internals.FExpr_R [ind, in mathcomp.algebra.field_tactic]
Internals.FExpr_R_map [prf, in mathcomp.algebra.field_tactic]
Internals.FF_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.Field [constr, in mathcomp.algebra.ring_tactic]
Internals.field_checker [abbrev, in mathcomp.algebra.field_tactic]
Internals.field_checker [abbrev, in mathcomp.algebra.field_tactic]
Internals.field_checker [abbrev, in mathcomp.algebra.field_tactic]
Internals.field_checker_map_int_of_Z [prf, in mathcomp.algebra.field_tactic]
Internals.field_checker_R [def, in mathcomp.algebra.field_tactic]
Internals.field_correct [prf, in mathcomp.algebra.field_tactic]
Internals.field_inv [def, in mathcomp.algebra.ring_tactic]
Internals.field_or_ring [ind, in mathcomp.algebra.ring_tactic]
Internals.Fnorm [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fnorm_R [def, in mathcomp.algebra.field_tactic]
Internals.fold_left_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.fold_right_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Formula_Q2Z [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Formula_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.Formula_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.fst_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.FTautoChecker_sound [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.GFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.GFormula_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.hex_uint_N_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.hold [def, in mathcomp.algebra.arithmetic_tactic]
Internals.I_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.IFF_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.iff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.IMPL_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.implb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.inv_id [def, in mathcomp.algebra.ring_tactic]
Internals.invi [def, in mathcomp.algebra.ring_tactic]
Internals.is_bool_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.is_bool_spec [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.is_boolP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.is_cnf_ff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.is_cnf_ffT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.is_cnf_tt_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.is_cnf_ttT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.is_tauto [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.is_tauto_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.is_tautoT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.is_true_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.isBool_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.IsBoolF [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.IsBoolNone [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.IsBoolT [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.isIn [abbrev, in mathcomp.algebra.field_tactic]
Internals.isIn_R [def, in mathcomp.algebra.field_tactic]
Internals.IsNeg_R [constr, in mathcomp.algebra.ring_tactic]
Internals.IsNul_R [constr, in mathcomp.algebra.ring_tactic]
Internals.IsPos_R [constr, in mathcomp.algebra.ring_tactic]
Internals.isProp_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.iter_op_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.KFeval [def, in mathcomp.algebra.arithmetic_tactic]
Internals.KFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.kind_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.large_nat [ind, in mathcomp.algebra.ring_tactic]
Internals.large_nat_dec_uint [constr, in mathcomp.algebra.ring_tactic]
Internals.large_nat_hex_uint [constr, in mathcomp.algebra.ring_tactic]
Internals.large_nat_N [constr, in mathcomp.algebra.ring_tactic]
Internals.large_nat_N_nat [prf, in mathcomp.algebra.ring_tactic]
Internals.large_nat_uint [constr, in mathcomp.algebra.ring_tactic]
Internals.linear_R [ind, in mathcomp.algebra.field_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.M0 [constr, in mathcomp.algebra.ring_tactic]
Internals.MAdd [constr, in mathcomp.algebra.ring_tactic]
Internals.MAdditive [constr, in mathcomp.algebra.ring_tactic]
Internals.map_option_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.map_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.mask_R [ind, in mathcomp.algebra.ring_tactic]
Internals.Meval [def, in mathcomp.algebra.ring_tactic]
Internals.Meval [abbrev, in mathcomp.algebra.ring_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.MExpr [ind, in mathcomp.algebra.ring_tactic]
Internals.MExpr_ind [scheme, in mathcomp.algebra.ring_tactic]
Internals.MExpr_ind' [def, in mathcomp.algebra.ring_tactic]
Internals.MExpr_rec [scheme, in mathcomp.algebra.ring_tactic]
Internals.MExpr_rect [scheme, in mathcomp.algebra.ring_tactic]
Internals.MExpr_sind [scheme, in mathcomp.algebra.ring_tactic]
Internals.MFactor [abbrev, in mathcomp.algebra.ring_tactic]
Internals.MFactor_R [def, in mathcomp.algebra.ring_tactic]
Internals.MintAdditive [constr, in mathcomp.algebra.ring_tactic]
Internals.mk_and_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.mk_iff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.mk_impl_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.mk_linear_R [constr, in mathcomp.algebra.field_tactic]
Internals.mk_monpol_list [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mk_monpol_list [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mk_monpol_list_R [def, in mathcomp.algebra.ring_tactic]
Internals.mk_or_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.mk_rsplit_R [constr, in mathcomp.algebra.field_tactic]
Internals.mkPinj_pred_R [def, in mathcomp.algebra.ring_tactic]
Internals.mkPinj_R [def, in mathcomp.algebra.ring_tactic]
Internals.mkPX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkPX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkPX_R [def, in mathcomp.algebra.ring_tactic]
Internals.mkVmon_R [def, in mathcomp.algebra.ring_tactic]
Internals.mkX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkX_R [def, in mathcomp.algebra.ring_tactic]
Internals.mkZmon_R [def, in mathcomp.algebra.ring_tactic]
Internals.MMuln [constr, in mathcomp.algebra.ring_tactic]
Internals.MMulz [constr, in mathcomp.algebra.ring_tactic]
Internals.MnatAdditive [constr, in mathcomp.algebra.ring_tactic]
Internals.Mnorm [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Mnorm [def, in mathcomp.algebra.ring_tactic]
Internals.mon0_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Mon_of_Pol [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Mon_of_Pol_R [def, in mathcomp.algebra.ring_tactic]
Internals.Mon_R [ind, in mathcomp.algebra.ring_tactic]
Internals.MOpp [constr, in mathcomp.algebra.ring_tactic]
Internals.mul_R [def, in mathcomp.algebra.field_tactic]
Internals.mulf_div_common [prf, in mathcomp.algebra.field_tactic]
Internals.MX [constr, in mathcomp.algebra.ring_tactic]
Internals.N0_R [constr, in mathcomp.algebra.ring_tactic]
Internals.N_of_large_nat [def, in mathcomp.algebra.ring_tactic]
Internals.N_R [ind, in mathcomp.algebra.ring_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_large_nat [def, in mathcomp.algebra.ring_tactic]
Internals.nat_of_N_expand [def, in mathcomp.algebra.ring_tactic]
Internals.nat_of_N_expandE [prf, in mathcomp.algebra.ring_tactic]
Internals.nat_of_pos_expand [def, in mathcomp.algebra.ring_tactic]
Internals.nat_of_pos_rec_expand [def, 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.negate [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.negate_aux [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.negate_aux_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.negb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.NFeval [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.NFeval [def, in mathcomp.algebra.arithmetic_tactic]
Internals.NFeval_normalise [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.nformula_plus_nformula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.nformula_plus_nformula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.NFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.nformula_times_nformula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.nformula_times_nformula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.NonEqual_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.NonStrict_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.norm_subst [abbrev, in mathcomp.algebra.ring_tactic]
Internals.norm_subst [abbrev, in mathcomp.algebra.ring_tactic]
Internals.norm_subst_R [def, in mathcomp.algebra.ring_tactic]
Internals.normalise [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.normalise [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.normalise_aux [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.normalise_aux_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.normalise_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.NOT_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.not_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.NPEadd [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEadd_R [def, in mathcomp.algebra.field_tactic]
Internals.NPEmul [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEmul_R [def, in mathcomp.algebra.field_tactic]
Internals.NPEopp [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEopp_R [def, in mathcomp.algebra.field_tactic]
Internals.NPEpow [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEpow_R [def, in mathcomp.algebra.field_tactic]
Internals.NPEsub [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEsub_R [def, in mathcomp.algebra.field_tactic]
Internals.Npos_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Nsemiring_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.nth_nth [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.nth_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.nth_R1 [def, in mathcomp.algebra.arithmetic_tactic]
Internals.num_R [def, in mathcomp.algebra.field_tactic]
Internals.numField_correct [prf, in mathcomp.algebra.field_tactic]
Internals.Op1_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.Op2_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.OpAdd_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.OpEq_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.OpGe_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.OpGt_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.OpLe_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.OpLt_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.OpMult_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.OpNEq_R [constr, in mathcomp.algebra.arithmetic_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_clause [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.or_clause_cnf [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.or_clause_cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.or_clause_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.or_clauseP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.or_cnf [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.or_cnf [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.or_cnf_aux [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.or_cnf_aux_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.or_cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.or_introl_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.or_intror_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.OR_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.or_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.orb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.P0 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P0 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P0 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P0_R [def, in mathcomp.algebra.ring_tactic]
Internals.P1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P1_R [def, in mathcomp.algebra.ring_tactic]
Internals.Padd [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Padd [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Padd_R [def, in mathcomp.algebra.ring_tactic]
Internals.PaddC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddC_R [def, in mathcomp.algebra.ring_tactic]
Internals.PaddI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddI_R [def, in mathcomp.algebra.ring_tactic]
Internals.PaddX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddX_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_A_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_absurd_PCond_R [def, in mathcomp.algebra.field_tactic]
Internals.param_add_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_add_term_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_addb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_and_cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_AND_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_and_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_andb_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_app_R [def, in mathcomp.algebra.field_tactic]
Internals.param_apply_option_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_BFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_BFKFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_BFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_bind_option2_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_bind_option_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Build_Formula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Ccnf_of_GFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_CFactor_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_check_inconsistent_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_check_normalised_formulas_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Cis_tauto_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_clause_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cltb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Cnegate_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cneqb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_checker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_ff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_negate_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_normalise_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_of_GFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_of_list_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_cnf_tt_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Cnormalise_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_compare_cont_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_compare_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_cond_norm_R [def, in mathcomp.algebra.field_tactic]
Internals.param_condition_R [def, in mathcomp.algebra.field_tactic]
Internals.param_conj_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_CTautoChecker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_CWeakChecker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_default_isIn_R [def, in mathcomp.algebra.field_tactic]
Internals.param_denum_R [def, in mathcomp.algebra.field_tactic]
Internals.param_double_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_double_pred_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_double_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_eAND_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eFF_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eIFF_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eIMPL_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eKind_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eNOT_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_env_nth_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eOR_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_EQ_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eq_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eq_refl_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eqb_R [def, in mathcomp.algebra.field_tactic]
Internals.param_eqb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eqb_R1 [def, in mathcomp.algebra.field_tactic]
Internals.param_Equal_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eTT_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eval_op2_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_eval_Psatz_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_False_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Fapp_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Fcons00_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Fcons0_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Fcons1_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Fcons2_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEadd_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEc_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEdiv_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEI_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEinv_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEmul_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEO_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEopp_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEpow_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FEsub_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Feval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_FEX_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FExpr_R [def, in mathcomp.algebra.field_tactic]
Internals.param_FF_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_field_checker_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Fnorm_R [def, in mathcomp.algebra.field_tactic]
Internals.param_fold_left_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_fold_right_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Formula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_fst_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_GFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_GFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_I_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_IFF_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_iff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_IMPL_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_implb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_is_bool_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_is_cnf_ff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_is_cnf_tt_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_is_tauto_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_is_true_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_isBool_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_isIn_R [def, in mathcomp.algebra.field_tactic]
Internals.param_IsNeg_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_IsNul_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_IsPos_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_isProp_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_iter_op_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_KFeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_kind_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_linear_R [def, in mathcomp.algebra.field_tactic]
Internals.param_map_option_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_map_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_MFactor_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mk_and_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_mk_iff_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_mk_impl_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_mk_linear_R [def, in mathcomp.algebra.field_tactic]
Internals.param_mk_monpol_list_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mk_or_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_mk_rsplit_R [def, in mathcomp.algebra.field_tactic]
Internals.param_mkPinj_pred_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mkPinj_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mkPX_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mkVmon_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mkX_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mkZmon_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mon0_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Mon_of_Pol_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Mon_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_mul_R [def, in mathcomp.algebra.field_tactic]
Internals.param_N0_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_N_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_negate_aux_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_negb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_nformula_plus_nformula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_NFormula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_nformula_times_nformula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_NonEqual_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_NonStrict_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_norm_subst_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_normalise_aux_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_normalise_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_NOT_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_not_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_NPEadd_R [def, in mathcomp.algebra.field_tactic]
Internals.param_NPEmul_R [def, in mathcomp.algebra.field_tactic]
Internals.param_NPEopp_R [def, in mathcomp.algebra.field_tactic]
Internals.param_NPEpow_R [def, in mathcomp.algebra.field_tactic]
Internals.param_NPEsub_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Npos_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_nth_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_nth_R1 [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_num_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Op1_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Op2_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpAdd_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpEq_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpGe_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpGt_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpLe_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpLt_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpMult_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OpNEq_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_or_clause_cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_or_clause_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_or_cnf_aux_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_or_cnf_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_or_introl_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_or_intror_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_OR_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_or_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_orb_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_P0_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_P1_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Padd_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PaddC_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PaddI_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PaddX_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Pc_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEadd_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEc_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEeval_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PEI_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEmul_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEO_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEopp_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEpow_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Peq_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEsimp_R [def, in mathcomp.algebra.field_tactic]
Internals.param_PEsub_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PEX_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PExpr_eq_R [def, in mathcomp.algebra.field_tactic]
Internals.param_PExpr_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_pexpr_times_nformula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Pinj_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Pmul_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PmulC_aux_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PmulC_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PmulI_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PNSubst1_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PNSubst_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PNSubstL_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Pol_of_PExpr_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Pol_of_PExpr_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Pol_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_POneSubst_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Popp_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_pos_sub_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_positive_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Ppow_N_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Ppow_pos_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_pred_double_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_pred_double_R1 [def, in mathcomp.algebra.ring_tactic]
Internals.param_pred_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_pred_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Psatz_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzAdd_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzC_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzIn_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzLet_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzMulC_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzMulE_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzSquare_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_PsatzZ_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Psquare_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_Psub_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PsubC_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PsubI_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PSubstL1_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PSubstL_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PsubX_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_PX_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_rev_append_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_ring_checker_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_rsplit_common_R [def, in mathcomp.algebra.field_tactic]
Internals.param_rsplit_left_R [def, in mathcomp.algebra.field_tactic]
Internals.param_rsplit_R [def, in mathcomp.algebra.field_tactic]
Internals.param_rsplit_right_R [def, in mathcomp.algebra.field_tactic]
Internals.param_split_aux_R [def, in mathcomp.algebra.field_tactic]
Internals.param_split_R [def, in mathcomp.algebra.field_tactic]
Internals.param_Strict_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_sub_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_succ_double_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_succ_double_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_succ_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_tauto_checker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_to_nat_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_triv_div_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_True_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_TT_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_vmon_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_X_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.param_xH_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_xI_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_xO_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Z0_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Z_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_zmon_pred_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_zmon_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Zneg_R [def, in mathcomp.algebra.ring_tactic]
Internals.param_Zpos_R [def, in mathcomp.algebra.ring_tactic]
Internals.Pc_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PCond [abbrev, in mathcomp.algebra.field_tactic]
Internals.PCond [abbrev, in mathcomp.algebra.field_tactic]
Internals.PCond [abbrev, in mathcomp.algebra.field_tactic]
Internals.PCond [abbrev, in mathcomp.algebra.field_tactic]
Internals.PCond [abbrev, in mathcomp.algebra.field_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.PEadd_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PEc_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.field_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.field_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.field_tactic]
Internals.PEeval [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.PEeval_default_isIn [prf, in mathcomp.algebra.field_tactic]
Internals.PEeval_eqs [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval_eqs [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval_eqs [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval_eqs [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PEeval_eqs [abbrev, in mathcomp.algebra.field_tactic]
Internals.PEeval_eqs [abbrev, in mathcomp.algebra.field_tactic]
Internals.PEeval_eqs [abbrev, 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_R [def, in mathcomp.algebra.arithmetic_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.PEI_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PEmap_id [prf, in mathcomp.algebra.field_tactic]
Internals.PEmul_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PEO_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PEopp_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PEpow_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Peq [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peq [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peq [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peq [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peq_R [def, in mathcomp.algebra.ring_tactic]
Internals.PEsimp [abbrev, in mathcomp.algebra.field_tactic]
Internals.PEsimp_R [def, in mathcomp.algebra.field_tactic]
Internals.PEsub_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.field_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.Peval [abbrev, in mathcomp.algebra.arithmetic_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.PEX_R [constr, in mathcomp.algebra.ring_tactic]
Internals.PExpr_eq [abbrev, in mathcomp.algebra.field_tactic]
Internals.PExpr_eq_R [def, in mathcomp.algebra.field_tactic]
Internals.PExpr_eqP [prf, in mathcomp.algebra.field_tactic]
Internals.PExpr_Q2Z [def, in mathcomp.algebra.arithmetic_tactic]
Internals.PExpr_R [ind, in mathcomp.algebra.ring_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.pexpr_times_nformula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.pexpr_times_nformula_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Pinj_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Pmul [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Pmul [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Pmul_R [def, in mathcomp.algebra.ring_tactic]
Internals.PmulC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PmulC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PmulC_aux [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PmulC_aux [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PmulC_aux_R [def, in mathcomp.algebra.ring_tactic]
Internals.PmulC_R [def, in mathcomp.algebra.ring_tactic]
Internals.PmulI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PmulI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PmulI_R [def, in mathcomp.algebra.ring_tactic]
Internals.PNSubst [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PNSubst1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PNSubst1_R [def, in mathcomp.algebra.ring_tactic]
Internals.PNSubst_R [def, in mathcomp.algebra.ring_tactic]
Internals.PNSubstL [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PNSubstL_R [def, in mathcomp.algebra.ring_tactic]
Internals.Pol_of_PExpr [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Pol_of_PExpr [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Pol_of_PExpr [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.Pol_of_PExpr_R [def, in mathcomp.algebra.ring_tactic]
Internals.Pol_of_PExpr_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Pol_Q2Z [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Pol_R [ind, in mathcomp.algebra.ring_tactic]
Internals.Pol_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.POneSubst [abbrev, in mathcomp.algebra.ring_tactic]
Internals.POneSubst_R [def, in mathcomp.algebra.ring_tactic]
Internals.Popp [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Popp_id [prf, in mathcomp.algebra.ring_tactic]
Internals.Popp_R [def, in mathcomp.algebra.ring_tactic]
Internals.Pos_add_R [def, in mathcomp.algebra.ring_tactic]
Internals.Pos_sub_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.pos_sub_R [def, in mathcomp.algebra.ring_tactic]
Internals.PosDA [prf, in mathcomp.algebra.ring_tactic]
Internals.positive_R [ind, 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.pow_pos [abbrev, in mathcomp.algebra.field_tactic]
Internals.pow_pos [abbrev, in mathcomp.algebra.field_tactic]
Internals.Ppow_N [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Ppow_N [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Ppow_N_R [def, in mathcomp.algebra.ring_tactic]
Internals.Ppow_pos [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Ppow_pos [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Ppow_pos_R [def, in mathcomp.algebra.ring_tactic]
Internals.pred_double_R [def, in mathcomp.algebra.ring_tactic]
Internals.pred_double_R1 [def, in mathcomp.algebra.ring_tactic]
Internals.pred_R [def, in mathcomp.algebra.ring_tactic]
Internals.pred_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Psatz_Q2Z [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Psatz_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.Psatz_R_map [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzAdd_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzC_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzIn_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzLet_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzMulC_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzMulE_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzSquare_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.PsatzZ_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.Psquare [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.Psquare_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Psub [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Psub_add [prf, in mathcomp.algebra.ring_tactic]
Internals.Psub_R [def, in mathcomp.algebra.ring_tactic]
Internals.PsubC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PsubC_R [def, in mathcomp.algebra.ring_tactic]
Internals.PsubI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PsubI_addI [prf, in mathcomp.algebra.ring_tactic]
Internals.PsubI_R [def, in mathcomp.algebra.ring_tactic]
Internals.PSubstL [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PSubstL1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PSubstL1_R [def, in mathcomp.algebra.ring_tactic]
Internals.PSubstL_R [def, in mathcomp.algebra.ring_tactic]
Internals.PsubX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PsubX_addX [prf, in mathcomp.algebra.ring_tactic]
Internals.PsubX_R [def, in mathcomp.algebra.ring_tactic]
Internals.PX_R [constr, in mathcomp.algebra.ring_tactic]
Internals.QTautoCheckerT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.R0 [constr, in mathcomp.algebra.ring_tactic]
Internals.R1 [constr, in mathcomp.algebra.ring_tactic]
Internals.R_of_N [abbrev, in mathcomp.algebra.ring_tactic]
Internals.R_of_N [def, in mathcomp.algebra.ring_tactic]
Internals.R_of_N_natmul [prf, in mathcomp.algebra.ring_tactic]
Internals.R_of_Q [def, in mathcomp.algebra.arithmetic_tactic]
Internals.R_of_Q_ratr [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.R_of_Z [abbrev, in mathcomp.algebra.ring_tactic]
Internals.R_of_Z [def, in mathcomp.algebra.ring_tactic]
Internals.R_of_Z [abbrev, in mathcomp.algebra.field_tactic]
Internals.R_of_Z [abbrev, in mathcomp.algebra.field_tactic]
Internals.R_of_Z_intr [prf, in mathcomp.algebra.ring_tactic]
Internals.RAdd [constr, in mathcomp.algebra.ring_tactic]
Internals.RAdditive [constr, in mathcomp.algebra.ring_tactic]
Internals.RBFeval [def, in mathcomp.algebra.arithmetic_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.rev_append_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Reval [def, in mathcomp.algebra.ring_tactic]
Internals.Reval_eqs [def, in mathcomp.algebra.ring_tactic]
Internals.Reval_formula [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Reval_op2 [def, in mathcomp.algebra.arithmetic_tactic]
Internals.RExpn [constr, in mathcomp.algebra.ring_tactic]
Internals.RExpNegz [constr, in mathcomp.algebra.ring_tactic]
Internals.RExpPosz [constr, in mathcomp.algebra.ring_tactic]
Internals.RExpr [ind, in mathcomp.algebra.ring_tactic]
Internals.RExpr_ind [scheme, in mathcomp.algebra.ring_tactic]
Internals.RExpr_ind' [def, in mathcomp.algebra.ring_tactic]
Internals.RExpr_rec [scheme, in mathcomp.algebra.ring_tactic]
Internals.RExpr_rect [scheme, in mathcomp.algebra.ring_tactic]
Internals.RExpr_sind [scheme, in mathcomp.algebra.ring_tactic]
Internals.RFeval [def, in mathcomp.algebra.arithmetic_tactic]
Internals.RFevalP [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.RFormula [rec, in mathcomp.algebra.arithmetic_tactic]
Internals.Ring [constr, in mathcomp.algebra.ring_tactic]
Internals.ring_checker [abbrev, in mathcomp.algebra.ring_tactic]
Internals.ring_checker [abbrev, in mathcomp.algebra.ring_tactic]
Internals.ring_checker [abbrev, in mathcomp.algebra.ring_tactic]
Internals.ring_checker [abbrev, in mathcomp.algebra.ring_tactic]
Internals.ring_checker_map_int_of_Z [prf, in mathcomp.algebra.ring_tactic]
Internals.ring_checker_R [def, in mathcomp.algebra.ring_tactic]
Internals.ring_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.ring_opp_intr [def, in mathcomp.algebra.ring_tactic]
Internals.RintAdditive [constr, in mathcomp.algebra.ring_tactic]
Internals.RintMorph [constr, in mathcomp.algebra.ring_tactic]
Internals.RInv [constr, in mathcomp.algebra.ring_tactic]
Internals.Rlhs [proj, in mathcomp.algebra.arithmetic_tactic]
Internals.RMorph [constr, in mathcomp.algebra.ring_tactic]
Internals.RMul [constr, in mathcomp.algebra.ring_tactic]
Internals.RMuln [constr, in mathcomp.algebra.ring_tactic]
Internals.RMulz [constr, in mathcomp.algebra.ring_tactic]
Internals.RnatAdd [constr, in mathcomp.algebra.ring_tactic]
Internals.RnatAdditive [constr, in mathcomp.algebra.ring_tactic]
Internals.RnatC [constr, in mathcomp.algebra.ring_tactic]
Internals.RnatExpn [constr, in mathcomp.algebra.ring_tactic]
Internals.RnatMorph [constr, in mathcomp.algebra.ring_tactic]
Internals.RnatMul [constr, in mathcomp.algebra.ring_tactic]
Internals.RnatS [constr, in mathcomp.algebra.ring_tactic]
Internals.RNegz [constr, in mathcomp.algebra.ring_tactic]
Internals.Rnorm [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Rnorm [def, 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_expr [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.Rnorm_formula [def, in mathcomp.algebra.arithmetic_tactic]
Internals.Rnorm_formula_correct [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.Rop [proj, in mathcomp.algebra.arithmetic_tactic]
Internals.ROpp [constr, in mathcomp.algebra.ring_tactic]
Internals.RPosz [constr, in mathcomp.algebra.ring_tactic]
Internals.Rrhs [proj, in mathcomp.algebra.arithmetic_tactic]
Internals.rsplit_common_R [def, in mathcomp.algebra.field_tactic]
Internals.rsplit_left_R [def, in mathcomp.algebra.field_tactic]
Internals.rsplit_R [ind, in mathcomp.algebra.field_tactic]
Internals.rsplit_right_R [def, in mathcomp.algebra.field_tactic]
Internals.RTautoChecker_sound [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.RX [constr, in mathcomp.algebra.ring_tactic]
Internals.sCring_checkerT [prf, in mathcomp.algebra.ring_tactic]
Internals.SemiRing [constr, 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.semiring_of_field_or_ring [def, in mathcomp.algebra.ring_tactic]
Internals.seq_Psatz_Q2Z [def, in mathcomp.algebra.arithmetic_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 [abbrev, in mathcomp.algebra.field_tactic]
Internals.split_aux [abbrev, in mathcomp.algebra.field_tactic]
Internals.split_aux_R [def, in mathcomp.algebra.field_tactic]
Internals.split_neq0_l [prf, in mathcomp.algebra.field_tactic]
Internals.split_neq0_r [prf, in mathcomp.algebra.field_tactic]
Internals.split_R [def, in mathcomp.algebra.field_tactic]
Internals.Strict_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.sub [abbrev, in mathcomp.algebra.field_tactic]
Internals.sub [abbrev, in mathcomp.algebra.field_tactic]
Internals.sub_R [def, in mathcomp.algebra.ring_tactic]
Internals.succ_double_mask_R [def, in mathcomp.algebra.ring_tactic]
Internals.succ_double_R [def, in mathcomp.algebra.ring_tactic]
Internals.succ_R [def, in mathcomp.algebra.ring_tactic]
Internals.tauto_checker [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.tauto_checker_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.tauto_checkerT [prf, in mathcomp.algebra.arithmetic_tactic]
Internals.to_nat_R [def, in mathcomp.algebra.arithmetic_tactic]
Internals.triv_div_R [def, in mathcomp.algebra.ring_tactic]
Internals.True_R [ind, in mathcomp.algebra.arithmetic_tactic]
Internals.TT_R [constr, 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.unsat [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.vmon_R [constr, in mathcomp.algebra.ring_tactic]
Internals.X_R [constr, in mathcomp.algebra.arithmetic_tactic]
Internals.xH_R [constr, in mathcomp.algebra.ring_tactic]
Internals.xI_R [constr, in mathcomp.algebra.ring_tactic]
Internals.xO_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Z0_R [constr, in mathcomp.algebra.ring_tactic]
Internals.z_const_helper [def, in mathcomp.algebra.ring_tactic]
Internals.Z_R [ind, in mathcomp.algebra.ring_tactic]
Internals.Zfield_correct [prf, in mathcomp.algebra.field_tactic]
Internals.Zint_pow_pos_pos [prf, in mathcomp.algebra.field_tactic]
Internals.zmon_pred_R [def, in mathcomp.algebra.ring_tactic]
Internals.zmon_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Zneg_R [constr, in mathcomp.algebra.ring_tactic]
Internals.ZnumField_correct [prf, in mathcomp.algebra.field_tactic]
Internals.Zpos_R [constr, in mathcomp.algebra.ring_tactic]
Internals.Zring_correct [prf, in mathcomp.algebra.ring_tactic]
Internals.ZTautoChecker [def, in mathcomp.algebra.arithmetic_tactic]
Internals.ZTautoCheckerT [prf, in mathcomp.algebra.arithmetic_tactic]
interval [file, in mathcomp.algebra.interval]
Interval [constr, in mathcomp.algebra.interval]
interval [ind, in mathcomp.algebra.interval]
interval_display [prf, in mathcomp.algebra.interval]
interval_inference [file, in mathcomp.algebra.interval_inference]
IntervalCan [mod, in mathcomp.algebra.interval]
IntervalCan.Exports [mod, 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 [mod, in mathcomp.algebra.interval_inference]
IntItv.add [def, in mathcomp.algebra.interval_inference]
IntItv.add_boundl [def, in mathcomp.algebra.interval_inference]
IntItv.add_boundr [def, in mathcomp.algebra.interval_inference]
IntItv.Empty [constr, in mathcomp.algebra.interval_inference]
IntItv.EqZero [constr, in mathcomp.algebra.interval_inference]
IntItv.exprn [def, in mathcomp.algebra.interval_inference]
IntItv.exprn_le1_bound [def, in mathcomp.algebra.interval_inference]
IntItv.exprz [def, in mathcomp.algebra.interval_inference]
IntItv.inv [def, in mathcomp.algebra.interval_inference]
IntItv.keep_neg_bound [def, in mathcomp.algebra.interval_inference]
IntItv.keep_nonneg [def, in mathcomp.algebra.interval_inference]
IntItv.keep_nonneg_bound [def, in mathcomp.algebra.interval_inference]
IntItv.keep_nonpos [def, in mathcomp.algebra.interval_inference]
IntItv.keep_nonpos_bound [def, in mathcomp.algebra.interval_inference]
IntItv.keep_pos_bound [def, in mathcomp.algebra.interval_inference]
IntItv.keep_sign [def, in mathcomp.algebra.interval_inference]
IntItv.Known [constr, in mathcomp.algebra.interval_inference]
IntItv.max [def, in mathcomp.algebra.interval_inference]
IntItv.min [def, in mathcomp.algebra.interval_inference]
IntItv.mul [def, in mathcomp.algebra.interval_inference]
IntItv.mul_boundl [def, in mathcomp.algebra.interval_inference]
IntItv.mul_boundr [def, in mathcomp.algebra.interval_inference]
IntItv.mul_boundr_gt0 [prf, in mathcomp.algebra.interval_inference]
IntItv.mul_boundrC [prf, in mathcomp.algebra.interval_inference]
IntItv.NonNeg [constr, in mathcomp.algebra.interval_inference]
IntItv.NonPos [constr, in mathcomp.algebra.interval_inference]
IntItv.opp [def, in mathcomp.algebra.interval_inference]
IntItv.opp_bound [def, 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]
IntItv.sign [def, in mathcomp.algebra.interval_inference]
IntItv.sign_boundl [def, in mathcomp.algebra.interval_inference]
IntItv.sign_boundr [def, in mathcomp.algebra.interval_inference]
IntItv.signb [ind, in mathcomp.algebra.interval_inference]
IntItv.signi [ind, in mathcomp.algebra.interval_inference]
IntItv.Unknown [constr, in mathcomp.algebra.interval_inference]
intmul [def, in mathcomp.algebra.ssrint]
intmul1_is_monoid_morphism [prf, in mathcomp.algebra.ssrint]
intmul1_is_multiplicative [def, in mathcomp.algebra.ssrint]
intOrdered [mod, in mathcomp.algebra.ssrint]
intOrdered.gez0_norm [prf, in mathcomp.algebra.ssrint]
intOrdered.lez [def, 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, in mathcomp.algebra.ssrint]
intOrdered.ltz_def [prf, in mathcomp.algebra.ssrint]
intOrdered.Mixin [def, in mathcomp.algebra.ssrint]
intOrdered.normz [abbrev, 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]
intr [abbrev, in mathcomp.algebra.ssrint]
intr1D [prf, in mathcomp.algebra.ssrint]
intr_eq0 [prf, in mathcomp.algebra.ssrint]
intr_inj [def, in mathcomp.algebra.ssrint]
intr_inj_ZtoC [def, in mathcomp.field.algnum]
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 [mod, in mathcomp.algebra.ssrint]
intRing.comMixin [def, 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.mulz [def, 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]
intrp [abbrev, in mathcomp.field.cyclotomic]
intrp [abbrev, in mathcomp.field.algnum]
intrp [abbrev, in mathcomp.field.algC]
intrV [prf, in mathcomp.algebra.ssrint]
intS [prf, in mathcomp.algebra.ssrint]
intUnitRing [mod, in mathcomp.algebra.ssrint]
intUnitRing.comMixin [def, in mathcomp.algebra.ssrint]
intUnitRing.idomain_axiomz [prf, in mathcomp.algebra.ssrint]
intUnitRing.invz [def, 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.unitz [def, in mathcomp.algebra.ssrint]
intUnitRing.unitzPl [prf, in mathcomp.algebra.ssrint]
intz [prf, in mathcomp.algebra.ssrint]
intZmod [mod, 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.addz [def, in mathcomp.algebra.ssrint]
intZmod.addzA [prf, in mathcomp.algebra.ssrint]
intZmod.addzC [prf, in mathcomp.algebra.ssrint]
intZmod.int_ind [def, in mathcomp.algebra.ssrint]
intZmod.int_rec [def, in mathcomp.algebra.ssrint]
intZmod.int_rect [prf, in mathcomp.algebra.ssrint]
intZmod.int_spec [ind, in mathcomp.algebra.ssrint]
intZmod.intP [prf, in mathcomp.algebra.ssrint]
intZmod.Mixin [def, in mathcomp.algebra.ssrint]
intZmod.NegzE [prf, in mathcomp.algebra.ssrint]
intZmod.oppz [def, 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]
intZmod.ZintNeg [constr, in mathcomp.algebra.ssrint]
intZmod.ZintNull [constr, in mathcomp.algebra.ssrint]
intZmod.ZintPos [constr, in mathcomp.algebra.ssrint]
inv [def, in mathcomp.boot.monoid]
inv_ahom [def, in mathcomp.field.galois]
inv_dprod_Iirr [def, in mathcomp.group_representation.character]
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, in mathcomp.algebra.vector]
inv_lfun_def [prf, in mathcomp.algebra.vector]
inv_pair [def, in mathcomp.boot.monoid]
inv_quotient_spec [ind, in mathcomp.finite_group.quotient]
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 [def, in mathcomp.boot.eqtype]
invariant_chief_irr_cases [prf, in mathcomp.group_representation.inertia]
invariant_comp [prf, in mathcomp.boot.eqtype]
invariant_factor [def, in mathcomp.solvable.gseries]
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]
InvClosed [abbrev, in mathcomp.boot.monoid]
InvClosed [mod, in mathcomp.boot.monoid]
InvClosed.axioms_ [rec, in mathcomp.boot.monoid]
InvClosed.class [proj, in mathcomp.boot.monoid]
InvClosed.clone [abbrev, in mathcomp.boot.monoid]
InvClosed.copy [abbrev, in mathcomp.boot.monoid]
InvClosed.Exports [mod, in mathcomp.boot.monoid]
InvClosed.Exports.invgClosed [abbrev, in mathcomp.boot.monoid]
InvClosed.monoid_isInvClosed_mixin [proj, in mathcomp.boot.monoid]
InvClosed.on [abbrev, in mathcomp.boot.monoid]
InvClosed.on_ [abbrev, in mathcomp.boot.monoid]
InvClosed.pack_ [def, in mathcomp.boot.monoid]
InvClosed.phant_clone [def, in mathcomp.boot.monoid]
InvClosed.phant_on_ [def, in mathcomp.boot.monoid]
InvClosed.sort [proj, in mathcomp.boot.monoid]
InvClosed.type [rec, in mathcomp.boot.monoid]
InvClosedElpiOperations [mod, in mathcomp.boot.monoid]
invDg [prf, in mathcomp.finite_group.fingroup]
invF [def, in mathcomp.boot.fintype]
invF_f [prf, in mathcomp.boot.fintype]
invg [abbrev, in mathcomp.finite_group.fingroup]
invg1 [abbrev, in mathcomp.finite_group.fingroup]
invg1 [prf, in mathcomp.boot.monoid]
invg2id [prf, in mathcomp.finite_group.fingroup]
invg_closed [def, in mathcomp.boot.monoid]
invg_comm [abbrev, 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 [abbrev, in mathcomp.finite_group.fingroup]
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]
invgK [abbrev, in mathcomp.finite_group.fingroup]
invgK [def, in mathcomp.boot.monoid]
invgM [def, in mathcomp.boot.monoid]
invgR [prf, in mathcomp.boot.monoid]
invIg [prf, in mathcomp.finite_group.fingroup]
invm [def, in mathcomp.finite_group.morphism]
invm_morphism [def, in mathcomp.finite_group.morphism]
invm_subker [prf, in mathcomp.finite_group.morphism]
invmE [prf, in mathcomp.finite_group.morphism]
invMG [prf, in mathcomp.finite_group.fingroup]
invMg [abbrev, in mathcomp.finite_group.fingroup]
invmK [prf, in mathcomp.finite_group.morphism]
invmx [def, in mathcomp.algebra.matrix]
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]
InvolutiveRMorphism [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism [mod, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.Algebra_isNmodMorphism_mixin [proj, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.axioms_ [rec, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.class [proj, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.clone [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.copy [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.Exports [mod, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.Exports.involutive_rmorphism [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.GRing_isMonoidMorphism_mixin [proj, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.on [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.on_ [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.pack_ [def, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.phant_clone [def, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.phant_on_ [def, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.sesquilinear_isInvolutive_mixin [proj, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.sort [proj, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.type [rec, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphismElpiOperations [mod, in mathcomp.algebra.sesquilinear]
invq [def, in mathcomp.algebra.rat]
invq0 [prf, in mathcomp.algebra.rat]
invq_def [prf, in mathcomp.algebra.rat]
invq_frac [prf, in mathcomp.algebra.rat]
invq_subdef [def, in mathcomp.algebra.rat]
InvQuotientSpec [constr, in mathcomp.finite_group.quotient]
invr_expz [prf, in mathcomp.algebra.ssrint]
invr_lin_char [prf, in mathcomp.group_representation.character]
invSg [prf, in mathcomp.finite_group.fingroup]
invt [def, in mathcomp.algebra.tensor]
invUg [prf, in mathcomp.finite_group.fingroup]
inZp [def, in mathcomp.boot.fintype]
inZp [abbrev, in mathcomp.algebra.zmodp]
IOne [constr, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Ione [ind, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
IOpp [constr, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
iota [def, in mathcomp.boot.seq]
iota_ltn_sorted [prf, in mathcomp.boot.path]
iota_sorted [prf, in mathcomp.boot.path]
iota_tuple [def, in mathcomp.boot.tuple]
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]
iotaPz [abbrev, in mathcomp.field.fieldext]
IRat [constr, in mathcomp.algebra.rat]
Irat [ind, in mathcomp.algebra.rat]
Irat_prf [ind, in mathcomp.algebra.rat]
irr [abbrev, in mathcomp.group_representation.character]
irr [mod, in mathcomp.group_representation.character]
irr.body [def, in mathcomp.group_representation.character]
irr.unlock [def, in mathcomp.group_representation.character]
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_class [def, in mathcomp.group_representation.character]
irr_classK [prf, in mathcomp.group_representation.character]
irr_classP [prf, in mathcomp.group_representation.character]
irr_comp [def, in mathcomp.group_representation.mxrepresentation]
irr_comp'_op0 [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_comp'_op0_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_comp_envelop [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_comp_envelop_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_comp_id [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_comp_id_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_comp_rsim [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_comp_rsim_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_constt [def, in mathcomp.group_representation.character]
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 [def, in mathcomp.group_representation.mxrepresentation]
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_Locked [modtype, in mathcomp.group_representation.character]
irr_Locked.body [ax, in mathcomp.group_representation.character]
irr_Locked.unlock [ax, in mathcomp.group_representation.character]
irr_mode [def, in mathcomp.group_representation.mxrepresentation]
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 [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_mx_mult_pchar [prf, in mathcomp.group_representation.mxrepresentation]
irr_mx_sum [abbrev, 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 [def, 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 [def, in mathcomp.group_representation.mxrepresentation]
irr_repr'_op0 [abbrev, in mathcomp.group_representation.mxrepresentation]
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 [abbrev, 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_unlock_subterm [def, 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]
irreducibleb [def, in mathcomp.algebra.qpoly]
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]
irrType [def, in mathcomp.group_representation.mxrepresentation]
irrWchar [prf, in mathcomp.group_representation.character]
irrWnorm [prf, in mathcomp.group_representation.character]
is_abelem [def, in mathcomp.solvable.abelian]
is_abelem_pgroup [prf, in mathcomp.solvable.abelian]
is_abelemP [prf, in mathcomp.solvable.abelian]
is_action [def, in mathcomp.finite_group.action]
is_algid [def, in mathcomp.field.falgebra]
is_aspace [def, in mathcomp.field.falgebra]
is_class_fun [def, in mathcomp.group_representation.classfun]
is_diag_block_mx [prf, in mathcomp.algebra.matrix]
is_diag_mx [def, 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_groupAction [def, in mathcomp.finite_group.action]
is_hermitianmxE [prf, in mathcomp.algebra.sesquilinear]
is_hermitianmxP [prf, in mathcomp.algebra.sesquilinear]
is_hermsym [def, in mathcomp.algebra.sesquilinear]
is_iso [def, in mathcomp.solvable.burnside_app]
is_iso3 [def, in mathcomp.solvable.burnside_app]
is_iso3b [def, in mathcomp.solvable.burnside_app]
is_iso3P [prf, in mathcomp.solvable.burnside_app]
is_isoP [prf, in mathcomp.solvable.burnside_app]
is_mxvec_index [ind, in mathcomp.algebra.matrix]
is_orthogonal [abbrev, in mathcomp.algebra.sesquilinear]
is_perm_mx [def, in mathcomp.algebra.matrix]
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_porthogonal [def, in mathcomp.algebra.sesquilinear]
is_psymplectic [def, in mathcomp.algebra.sesquilinear]
is_rot [def, in mathcomp.solvable.burnside_app]
is_scalar_mx [def, 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_skew [def, in mathcomp.algebra.sesquilinear]
is_sym [def, in mathcomp.algebra.sesquilinear]
is_symplectic [abbrev, in mathcomp.algebra.sesquilinear]
is_total_action [prf, in mathcomp.finite_group.action]
is_transversal [def, in mathcomp.boot.finset]
is_trig_block_mx [prf, in mathcomp.algebra.matrix]
is_trig_mx [def, 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]
is_unitary [def, in mathcomp.algebra.sesquilinear]
isBilinear [abbrev, in mathcomp.algebra.sesquilinear]
isBilinear [mod, in mathcomp.algebra.sesquilinear]
isBilinear.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isBilinear.axioms_ [rec, in mathcomp.algebra.sesquilinear]
isBilinear.Build [abbrev, in mathcomp.algebra.sesquilinear]
isBilinear.Exports [mod, in mathcomp.algebra.sesquilinear]
isBilinear.identity_builder [def, in mathcomp.algebra.sesquilinear]
isBilinear.phant_axioms [def, in mathcomp.algebra.sesquilinear]
isBilinear.phant_Build [def, in mathcomp.algebra.sesquilinear]
isComplex [abbrev, in mathcomp.field.algC]
isComplex [mod, in mathcomp.field.algC]
isComplex.axioms [abbrev, in mathcomp.field.algC]
isComplex.axioms_ [rec, in mathcomp.field.algC]
isComplex.Build [abbrev, in mathcomp.field.algC]
isComplex.conj [proj, in mathcomp.field.algC]
isComplex.conj_nt [proj, in mathcomp.field.algC]
isComplex.conjK [proj, in mathcomp.field.algC]
isComplex.Exports [mod, in mathcomp.field.algC]
isComplex.phant_axioms [def, in mathcomp.field.algC]
isComplex.phant_Build [def, in mathcomp.field.algC]
isCountable [abbrev, in mathcomp.boot.choice]
isCountable [mod, in mathcomp.boot.choice]
isCountable.axioms [abbrev, in mathcomp.boot.choice]
isCountable.axioms_ [rec, in mathcomp.boot.choice]
isCountable.Build [abbrev, in mathcomp.boot.choice]
isCountable.Exports [mod, in mathcomp.boot.choice]
isCountable.phant_axioms [def, in mathcomp.boot.choice]
isCountable.phant_Build [def, in mathcomp.boot.choice]
isCountable.pickle [proj, in mathcomp.boot.choice]
isCountable.pickleK [proj, in mathcomp.boot.choice]
isCountable.unpickle [proj, in mathcomp.boot.choice]
isDotProduct [abbrev, in mathcomp.algebra.sesquilinear]
isDotProduct [mod, in mathcomp.algebra.sesquilinear]
isDotProduct.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isDotProduct.axioms_ [rec, in mathcomp.algebra.sesquilinear]
isDotProduct.Build [abbrev, in mathcomp.algebra.sesquilinear]
isDotProduct.Exports [mod, in mathcomp.algebra.sesquilinear]
isDotProduct.identity_builder [def, in mathcomp.algebra.sesquilinear]
isDotProduct.neq0_dnorm_gt0 [proj, in mathcomp.algebra.sesquilinear]
isDotProduct.phant_axioms [def, in mathcomp.algebra.sesquilinear]
isDotProduct.phant_Build [def, in mathcomp.algebra.sesquilinear]
isEqQuotient [abbrev, in mathcomp.boot.generic_quotient]
isEqQuotient [mod, in mathcomp.boot.generic_quotient]
isEqQuotient.axioms [abbrev, in mathcomp.boot.generic_quotient]
isEqQuotient.axioms_ [rec, in mathcomp.boot.generic_quotient]
isEqQuotient.Build [abbrev, in mathcomp.boot.generic_quotient]
isEqQuotient.Exports [mod, in mathcomp.boot.generic_quotient]
isEqQuotient.identity_builder [def, in mathcomp.boot.generic_quotient]
isEqQuotient.phant_axioms [def, in mathcomp.boot.generic_quotient]
isEqQuotient.phant_Build [def, in mathcomp.boot.generic_quotient]
isEqQuotient.pi_eq_quot [proj, in mathcomp.boot.generic_quotient]
isFinite [abbrev, in mathcomp.boot.fintype]
isFinite [mod, in mathcomp.boot.fintype]
isFinite.axioms [abbrev, in mathcomp.boot.fintype]
isFinite.axioms_ [rec, in mathcomp.boot.fintype]
isFinite.Build [abbrev, in mathcomp.boot.fintype]
isFinite.enum_subdef [proj, in mathcomp.boot.fintype]
isFinite.enumP_subdef [proj, in mathcomp.boot.fintype]
isFinite.Exports [mod, in mathcomp.boot.fintype]
isFinite.identity_builder [def, in mathcomp.boot.fintype]
isFinite.phant_axioms [def, in mathcomp.boot.fintype]
isFinite.phant_Build [def, in mathcomp.boot.fintype]
isGroup [abbrev, in mathcomp.boot.monoid]
isGroup [mod, in mathcomp.boot.monoid]
isGroup.axioms [abbrev, in mathcomp.boot.monoid]
isGroup.axioms_ [rec, in mathcomp.boot.monoid]
isGroup.Build [abbrev, in mathcomp.boot.monoid]
isGroup.Exports [mod, in mathcomp.boot.monoid]
isGroup.inv [proj, in mathcomp.boot.monoid]
isGroup.mul [proj, in mathcomp.boot.monoid]
isGroup.mul1g [proj, in mathcomp.boot.monoid]
isGroup.mulg1 [proj, in mathcomp.boot.monoid]
isGroup.mulgA [proj, in mathcomp.boot.monoid]
isGroup.mulgV [proj, in mathcomp.boot.monoid]
isGroup.mulVg [proj, in mathcomp.boot.monoid]
isGroup.one [proj, in mathcomp.boot.monoid]
isGroup.phant_axioms [def, in mathcomp.boot.monoid]
isGroup.phant_Build [def, in mathcomp.boot.monoid]
isGroupMorphism [abbrev, in mathcomp.boot.monoid]
isGroupMorphism [mod, in mathcomp.boot.monoid]
isGroupMorphism.axioms [abbrev, in mathcomp.boot.monoid]
isGroupMorphism.axioms_ [rec, in mathcomp.boot.monoid]
isGroupMorphism.Build [abbrev, in mathcomp.boot.monoid]
isGroupMorphism.Exports [mod, in mathcomp.boot.monoid]
isGroupMorphism.gmulfF [proj, in mathcomp.boot.monoid]
isGroupMorphism.phant_axioms [def, in mathcomp.boot.monoid]
isGroupMorphism.phant_Build [def, in mathcomp.boot.monoid]
isgroupP [prf, in mathcomp.finite_group.fingroup]
isHermitianSesquilinear [abbrev, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear [mod, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.axioms_ [rec, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.Build [abbrev, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.Exports [mod, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.identity_builder [def, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.phant_axioms [def, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.phant_Build [def, in mathcomp.algebra.sesquilinear]
isIdealr [abbrev, in mathcomp.algebra.ring_quotient]
isIdealr [mod, in mathcomp.algebra.ring_quotient]
isIdealr.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isIdealr.axioms_ [rec, in mathcomp.algebra.ring_quotient]
isIdealr.Build [abbrev, in mathcomp.algebra.ring_quotient]
isIdealr.Exports [mod, in mathcomp.algebra.ring_quotient]
isIdealr.phant_axioms [def, in mathcomp.algebra.ring_quotient]
isIdealr.phant_Build [def, in mathcomp.algebra.ring_quotient]
isInvClosed [abbrev, in mathcomp.boot.monoid]
isInvClosed [mod, in mathcomp.boot.monoid]
isInvClosed.axioms [abbrev, in mathcomp.boot.monoid]
isInvClosed.axioms_ [rec, in mathcomp.boot.monoid]
isInvClosed.Build [abbrev, in mathcomp.boot.monoid]
isInvClosed.Exports [mod, in mathcomp.boot.monoid]
isInvClosed.gpredVr [proj, in mathcomp.boot.monoid]
isInvClosed.identity_builder [def, in mathcomp.boot.monoid]
isInvClosed.phant_axioms [def, in mathcomp.boot.monoid]
isInvClosed.phant_Build [def, in mathcomp.boot.monoid]
isInvolutive [abbrev, in mathcomp.algebra.sesquilinear]
isInvolutive [mod, in mathcomp.algebra.sesquilinear]
isInvolutive.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isInvolutive.axioms_ [rec, in mathcomp.algebra.sesquilinear]
isInvolutive.Build [abbrev, in mathcomp.algebra.sesquilinear]
isInvolutive.Exports [mod, in mathcomp.algebra.sesquilinear]
isInvolutive.identity_builder [def, in mathcomp.algebra.sesquilinear]
isInvolutive.phant_axioms [def, in mathcomp.algebra.sesquilinear]
isInvolutive.phant_Build [def, in mathcomp.algebra.sesquilinear]
isMonoid [abbrev, in mathcomp.boot.monoid]
isMonoid [mod, in mathcomp.boot.monoid]
isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
isMonoid.axioms_ [rec, in mathcomp.boot.monoid]
isMonoid.Build [abbrev, in mathcomp.boot.monoid]
isMonoid.Exports [mod, in mathcomp.boot.monoid]
isMonoid.mul [proj, in mathcomp.boot.monoid]
isMonoid.mul1g [proj, in mathcomp.boot.monoid]
isMonoid.mulg1 [proj, in mathcomp.boot.monoid]
isMonoid.mulgA [proj, in mathcomp.boot.monoid]
isMonoid.one [proj, in mathcomp.boot.monoid]
isMonoid.phant_axioms [def, in mathcomp.boot.monoid]
isMonoid.phant_Build [def, in mathcomp.boot.monoid]
isMul1Closed [abbrev, in mathcomp.boot.monoid]
isMul1Closed [mod, in mathcomp.boot.monoid]
isMul1Closed.axioms [abbrev, in mathcomp.boot.monoid]
isMul1Closed.axioms_ [rec, in mathcomp.boot.monoid]
isMul1Closed.Build [abbrev, in mathcomp.boot.monoid]
isMul1Closed.Exports [mod, in mathcomp.boot.monoid]
isMul1Closed.gpred1 [proj, in mathcomp.boot.monoid]
isMul1Closed.identity_builder [def, in mathcomp.boot.monoid]
isMul1Closed.phant_axioms [def, in mathcomp.boot.monoid]
isMul1Closed.phant_Build [def, in mathcomp.boot.monoid]
isMulBaseGroup [abbrev, in mathcomp.finite_group.fingroup]
isMulBaseGroup [mod, in mathcomp.finite_group.fingroup]
isMulBaseGroup.Build [abbrev, in mathcomp.finite_group.fingroup]
isMulClosed [abbrev, in mathcomp.boot.monoid]
isMulClosed [mod, in mathcomp.boot.monoid]
isMulClosed.axioms [abbrev, in mathcomp.boot.monoid]
isMulClosed.axioms_ [rec, in mathcomp.boot.monoid]
isMulClosed.Build [abbrev, in mathcomp.boot.monoid]
isMulClosed.Exports [mod, in mathcomp.boot.monoid]
isMulClosed.gpredM [proj, in mathcomp.boot.monoid]
isMulClosed.identity_builder [def, in mathcomp.boot.monoid]
isMulClosed.phant_axioms [def, in mathcomp.boot.monoid]
isMulClosed.phant_Build [def, in mathcomp.boot.monoid]
isMulGroup [abbrev, in mathcomp.finite_group.fingroup]
isMulGroup [mod, in mathcomp.finite_group.fingroup]
isMulGroup.Build [abbrev, in mathcomp.finite_group.fingroup]
isMultiplicative [abbrev, in mathcomp.boot.monoid]
isMultiplicative [mod, in mathcomp.boot.monoid]
isMultiplicative.axioms [abbrev, in mathcomp.boot.monoid]
isMultiplicative.axioms_ [rec, in mathcomp.boot.monoid]
isMultiplicative.Build [abbrev, in mathcomp.boot.monoid]
isMultiplicative.Exports [mod, in mathcomp.boot.monoid]
isMultiplicative.gmulfM [proj, in mathcomp.boot.monoid]
isMultiplicative.identity_builder [def, in mathcomp.boot.monoid]
isMultiplicative.phant_axioms [def, in mathcomp.boot.monoid]
isMultiplicative.phant_Build [def, in mathcomp.boot.monoid]
isMxvecIndex [constr, in mathcomp.algebra.matrix]
IsNonneg [constr, in mathcomp.algebra.interval_inference]
isNzRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isNzRingQuotient [mod, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.axioms_ [rec, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.Exports [mod, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.identity_builder [def, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.phant_axioms [def, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.phant_Build [def, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.pi_mulr [proj, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.pi_oner [proj, in mathcomp.algebra.ring_quotient]
iso0_1 [prf, in mathcomp.solvable.burnside_app]
iso2_group [def, in mathcomp.solvable.burnside_app]
iso3 [def, in mathcomp.solvable.burnside_app]
iso3_ndir [prf, in mathcomp.solvable.burnside_app]
iso3l [def, 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]
iso_group [def, in mathcomp.solvable.burnside_app]
iso_group3 [def, in mathcomp.solvable.burnside_app]
isob [abbrev, in mathcomp.solvable.center]
isog [def, in mathcomp.finite_group.morphism]
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 [def, in mathcomp.finite_group.morphism]
isom_card [prf, in mathcomp.finite_group.morphism]
isom_cast_perm [prf, in mathcomp.finite_group.perm]
isom_Iirr [def, in mathcomp.group_representation.character]
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_inv [def, 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 [def, in mathcomp.solvable.burnside_app]
isometries2 [def, in mathcomp.solvable.burnside_app]
isometries_iso [prf, in mathcomp.solvable.burnside_app]
isometry [def, in mathcomp.group_representation.classfun]
isometry [def, in mathcomp.algebra.sesquilinear]
isometry_from_to [def, in mathcomp.group_representation.classfun]
isometry_from_to [def, in mathcomp.algebra.sesquilinear]
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]
IsPosnum [constr, in mathcomp.algebra.interval_inference]
isPrimeIdealrClosed [abbrev, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed [mod, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.axioms_ [rec, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.Build [abbrev, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.Exports [mod, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.identity_builder [def, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.phant_axioms [def, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.phant_Build [def, in mathcomp.algebra.ring_quotient]
isProperIdeal [abbrev, in mathcomp.algebra.ring_quotient]
isProperIdeal [mod, in mathcomp.algebra.ring_quotient]
isProperIdeal.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isProperIdeal.axioms_ [rec, in mathcomp.algebra.ring_quotient]
isProperIdeal.Build [abbrev, in mathcomp.algebra.ring_quotient]
isProperIdeal.Exports [mod, in mathcomp.algebra.ring_quotient]
isProperIdeal.identity_builder [def, in mathcomp.algebra.ring_quotient]
isProperIdeal.phant_axioms [def, in mathcomp.algebra.ring_quotient]
isProperIdeal.phant_Build [def, in mathcomp.algebra.ring_quotient]
isQuotient [abbrev, in mathcomp.boot.generic_quotient]
isQuotient [mod, in mathcomp.boot.generic_quotient]
isQuotient.axioms [abbrev, in mathcomp.boot.generic_quotient]
isQuotient.axioms_ [rec, in mathcomp.boot.generic_quotient]
isQuotient.Build [abbrev, in mathcomp.boot.generic_quotient]
isQuotient.Exports [mod, in mathcomp.boot.generic_quotient]
isQuotient.identity_builder [def, in mathcomp.boot.generic_quotient]
isQuotient.phant_axioms [def, in mathcomp.boot.generic_quotient]
isQuotient.phant_Build [def, in mathcomp.boot.generic_quotient]
isQuotient.quot_pi_subdef [proj, in mathcomp.boot.generic_quotient]
isQuotient.repr_of [proj, in mathcomp.boot.generic_quotient]
isRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isRingQuotient [mod, in mathcomp.algebra.ring_quotient]
isRingQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
isSemigroup [abbrev, in mathcomp.boot.monoid]
isSemigroup [mod, in mathcomp.boot.monoid]
isSemigroup.axioms [abbrev, in mathcomp.boot.monoid]
isSemigroup.axioms_ [rec, in mathcomp.boot.monoid]
isSemigroup.Build [abbrev, in mathcomp.boot.monoid]
isSemigroup.Exports [mod, in mathcomp.boot.monoid]
isSemigroup.mul [proj, in mathcomp.boot.monoid]
isSemigroup.mulgA [proj, in mathcomp.boot.monoid]
isSemigroup.phant_axioms [def, in mathcomp.boot.monoid]
isSemigroup.phant_Build [def, in mathcomp.boot.monoid]
isSome_insub [prf, in mathcomp.boot.eqtype]
isStarMonoid [abbrev, in mathcomp.boot.monoid]
isStarMonoid [mod, in mathcomp.boot.monoid]
isStarMonoid.axioms [abbrev, in mathcomp.boot.monoid]
isStarMonoid.axioms_ [rec, in mathcomp.boot.monoid]
isStarMonoid.Build [abbrev, in mathcomp.boot.monoid]
isStarMonoid.Exports [mod, in mathcomp.boot.monoid]
isStarMonoid.inv [proj, in mathcomp.boot.monoid]
isStarMonoid.invgK [proj, in mathcomp.boot.monoid]
isStarMonoid.invgM [proj, in mathcomp.boot.monoid]
isStarMonoid.mul [proj, in mathcomp.boot.monoid]
isStarMonoid.mul1g [proj, in mathcomp.boot.monoid]
isStarMonoid.mulgA [proj, in mathcomp.boot.monoid]
isStarMonoid.one [proj, in mathcomp.boot.monoid]
isStarMonoid.phant_axioms [def, in mathcomp.boot.monoid]
isStarMonoid.phant_Build [def, in mathcomp.boot.monoid]
isSub [abbrev, in mathcomp.boot.eqtype]
isSub [mod, in mathcomp.boot.eqtype]
isSub.axioms [abbrev, in mathcomp.boot.eqtype]
isSub.axioms_ [rec, in mathcomp.boot.eqtype]
isSub.Build [abbrev, in mathcomp.boot.eqtype]
isSub.Exports [mod, in mathcomp.boot.eqtype]
isSub.identity_builder [def, in mathcomp.boot.eqtype]
isSub.phant_axioms [def, in mathcomp.boot.eqtype]
isSub.phant_Build [def, in mathcomp.boot.eqtype]
isSub.Sub [proj, in mathcomp.boot.eqtype]
isSub.Sub_rect [proj, in mathcomp.boot.eqtype]
isSub.val_subdef [proj, in mathcomp.boot.eqtype]
isSubBaseUMagma [abbrev, in mathcomp.boot.monoid]
isSubBaseUMagma [mod, in mathcomp.boot.monoid]
isSubBaseUMagma.axioms [abbrev, in mathcomp.boot.monoid]
isSubBaseUMagma.axioms_ [rec, in mathcomp.boot.monoid]
isSubBaseUMagma.Build [abbrev, in mathcomp.boot.monoid]
isSubBaseUMagma.Exports [mod, in mathcomp.boot.monoid]
isSubBaseUMagma.identity_builder [def, in mathcomp.boot.monoid]
isSubBaseUMagma.phant_axioms [def, in mathcomp.boot.monoid]
isSubBaseUMagma.phant_Build [def, in mathcomp.boot.monoid]
isSubMagma [abbrev, in mathcomp.boot.monoid]
isSubMagma [mod, in mathcomp.boot.monoid]
isSubMagma.axioms [abbrev, in mathcomp.boot.monoid]
isSubMagma.axioms_ [rec, in mathcomp.boot.monoid]
isSubMagma.Build [abbrev, in mathcomp.boot.monoid]
isSubMagma.Exports [mod, in mathcomp.boot.monoid]
isSubMagma.identity_builder [def, in mathcomp.boot.monoid]
isSubMagma.phant_axioms [def, in mathcomp.boot.monoid]
isSubMagma.phant_Build [def, in mathcomp.boot.monoid]
isUMagmaMorphism [abbrev, in mathcomp.boot.monoid]
isUMagmaMorphism [mod, in mathcomp.boot.monoid]
isUMagmaMorphism.axioms [abbrev, in mathcomp.boot.monoid]
isUMagmaMorphism.axioms_ [rec, in mathcomp.boot.monoid]
isUMagmaMorphism.Build [abbrev, in mathcomp.boot.monoid]
isUMagmaMorphism.Exports [mod, in mathcomp.boot.monoid]
isUMagmaMorphism.phant_axioms [def, in mathcomp.boot.monoid]
isUMagmaMorphism.phant_Build [def, in mathcomp.boot.monoid]
isUnitRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient [mod, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.axioms_ [rec, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.Exports [mod, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.identity_builder [def, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.phant_axioms [def, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.phant_Build [def, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.pi_invr [proj, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.pi_unitr [proj, in mathcomp.algebra.ring_quotient]
isZmodQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isZmodQuotient [mod, in mathcomp.algebra.ring_quotient]
isZmodQuotient.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isZmodQuotient.axioms_ [rec, in mathcomp.algebra.ring_quotient]
isZmodQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
isZmodQuotient.Exports [mod, in mathcomp.algebra.ring_quotient]
isZmodQuotient.identity_builder [def, in mathcomp.algebra.ring_quotient]
isZmodQuotient.phant_axioms [def, in mathcomp.algebra.ring_quotient]
isZmodQuotient.phant_Build [def, in mathcomp.algebra.ring_quotient]
isZmodQuotient.pi_addr [proj, in mathcomp.algebra.ring_quotient]
isZmodQuotient.pi_oppr [proj, in mathcomp.algebra.ring_quotient]
isZmodQuotient.pi_zeror [proj, in mathcomp.algebra.ring_quotient]
iter [def, in mathcomp.boot.ssrnat]
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]
iteri [def, in mathcomp.boot.ssrnat]
iteriS [prf, in mathcomp.boot.ssrnat]
iterM [prf, in mathcomp.boot.ssrnat]
iterop [def, 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 [abbrev, in mathcomp.algebra.interval_inference]
Itv [mod, in mathcomp.algebra.interval_inference]
Itv.allP [proj, in mathcomp.algebra.interval_inference]
Itv.def [rec, in mathcomp.algebra.interval_inference]
Itv.Exports [mod, in mathcomp.algebra.interval_inference]
Itv.Exports.num [abbrev, in mathcomp.algebra.interval_inference]
Itv.from [def, in mathcomp.algebra.interval_inference]
Itv.fromP [def, in mathcomp.algebra.interval_inference]
Itv.mk [def, in mathcomp.algebra.interval_inference]
Itv.nat_sem [def, in mathcomp.algebra.interval_inference]
Itv.nonneg [def, in mathcomp.algebra.interval_inference]
Itv.num_sem [def, in mathcomp.algebra.interval_inference]
Itv.P [proj, in mathcomp.algebra.interval_inference]
Itv.posnum [def, in mathcomp.algebra.interval_inference]
Itv.r [proj, in mathcomp.algebra.interval_inference]
Itv.Real [constr, in mathcomp.algebra.interval_inference]
Itv.real1 [def, in mathcomp.algebra.interval_inference]
Itv.real2 [def, in mathcomp.algebra.interval_inference]
Itv.sort [proj, in mathcomp.algebra.interval_inference]
Itv.sort_sem [proj, in mathcomp.algebra.interval_inference]
Itv.spec [def, in mathcomp.algebra.interval_inference]
Itv.spec_real1 [prf, in mathcomp.algebra.interval_inference]
Itv.spec_real2 [prf, in mathcomp.algebra.interval_inference]
Itv.sub [def, in mathcomp.algebra.interval_inference]
Itv.t [ind, in mathcomp.algebra.interval_inference]
Itv.Top [constr, in mathcomp.algebra.interval_inference]
Itv.typ [rec, in mathcomp.algebra.interval_inference]
Itv01 [def, in mathcomp.algebra.interval_inference]
itv01_subdef [prf, in mathcomp.algebra.interval_inference]
itv_bound [ind, in mathcomp.algebra.interval]
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_decompose [def, in mathcomp.algebra.interval]
itv_ge [prf, in mathcomp.algebra.interval]
itv_join [def, 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_meet [def, 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_rewrite [def, 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 [def, in mathcomp.algebra.interval_inference]
itvnum_subdef [prf, in mathcomp.algebra.interval_inference]
itvP [prf, in mathcomp.algebra.interval]
itvPredType [def, in mathcomp.algebra.interval]
ItvReal [def, in mathcomp.algebra.interval_inference]
itvreal_subdef [prf, in mathcomp.algebra.interval_inference]
itvxx [prf, in mathcomp.algebra.interval]
itvxxP [prf, in mathcomp.algebra.interval]