| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (100113 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1864 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49278 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1631 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6978 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (94 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14781 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (131 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2030 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2189 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1149 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19126 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (565 entries) |
P (lemma)
PackSocleK [in mathcomp.character.mxrepresentation]pairg1_morphM [in mathcomp.fingroup.gproduct]
pairmapK [in mathcomp.ssreflect.seq]
pairmap_bseqP [in mathcomp.ssreflect.tuple]
pairmap_tupleP [in mathcomp.ssreflect.tuple]
pairmap_cat [in mathcomp.ssreflect.seq]
pairMnE [in mathcomp.algebra.ssralg]
pairwiseP [in mathcomp.ssreflect.seq]
pairwise_trans [in mathcomp.ssreflect.seq]
pairwise_eq [in mathcomp.ssreflect.seq]
pairwise_uniq [in mathcomp.ssreflect.seq]
pairwise_relI [in mathcomp.ssreflect.seq]
pairwise_map [in mathcomp.ssreflect.seq]
pairwise_all2rel [in mathcomp.ssreflect.seq]
pairwise_filter [in mathcomp.ssreflect.seq]
pairwise_mask [in mathcomp.ssreflect.seq]
pairwise_rcons [in mathcomp.ssreflect.seq]
pairwise_cat [in mathcomp.ssreflect.seq]
pairwise_cons [in mathcomp.ssreflect.seq]
pairwise_orthogonal_cat [in mathcomp.character.classfun]
pairwise_orthogonalP [in mathcomp.character.classfun]
pairwise_sort [in mathcomp.ssreflect.path]
pairwise_sorted [in mathcomp.ssreflect.path]
pairwise2 [in mathcomp.ssreflect.seq]
pair_of_tagK [in mathcomp.ssreflect.choice]
pair_invr_out [in mathcomp.algebra.ssralg]
pair_unitP [in mathcomp.algebra.ssralg]
pair_mulVr [in mathcomp.algebra.ssralg]
pair_mulVl [in mathcomp.algebra.ssralg]
pair_scaleAr [in mathcomp.algebra.ssralg]
pair_scaleAl [in mathcomp.algebra.ssralg]
pair_scaleDl [in mathcomp.algebra.ssralg]
pair_scaleDr [in mathcomp.algebra.ssralg]
pair_scale1 [in mathcomp.algebra.ssralg]
pair_scaleA [in mathcomp.algebra.ssralg]
pair_mulC [in mathcomp.algebra.ssralg]
pair_one_neq0 [in mathcomp.algebra.ssralg]
pair_mulr0 [in mathcomp.algebra.ssralg]
pair_mul0r [in mathcomp.algebra.ssralg]
pair_mulDr [in mathcomp.algebra.ssralg]
pair_mulDl [in mathcomp.algebra.ssralg]
pair_mul1r [in mathcomp.algebra.ssralg]
pair_mul1l [in mathcomp.algebra.ssralg]
pair_mulA [in mathcomp.algebra.ssralg]
pair_addN [in mathcomp.algebra.ssralg]
pair_add0 [in mathcomp.algebra.ssralg]
pair_addC [in mathcomp.algebra.ssralg]
pair_addA [in mathcomp.algebra.ssralg]
pair_vect_iso [in mathcomp.algebra.vector]
pair_bigA [in mathcomp.ssreflect.bigop]
pair_big [in mathcomp.ssreflect.bigop]
pair_big_dep [in mathcomp.ssreflect.bigop]
pair_bigA_idem [in mathcomp.ssreflect.bigop]
pair_big_idem [in mathcomp.ssreflect.bigop]
pair_big_dep_idem [in mathcomp.ssreflect.bigop]
pair_eq2 [in mathcomp.ssreflect.eqtype]
pair_eq1 [in mathcomp.ssreflect.eqtype]
pair_eqE [in mathcomp.ssreflect.eqtype]
pair_eqP [in mathcomp.ssreflect.eqtype]
pair1g_morphM [in mathcomp.fingroup.gproduct]
partG_eq1 [in mathcomp.solvable.pgroup]
partitionD1 [in mathcomp.ssreflect.finset]
partitionS [in mathcomp.ssreflect.finset]
partitionU1 [in mathcomp.ssreflect.finset]
partition_partition [in mathcomp.ssreflect.finset]
partition_disjoint_bigcup [in mathcomp.ssreflect.finset]
partition_pigeonhole [in mathcomp.ssreflect.finset]
partition_set0 [in mathcomp.ssreflect.finset]
partition_trivIset [in mathcomp.ssreflect.finset]
partition_neq0 [in mathcomp.ssreflect.finset]
partition_big_imset [in mathcomp.ssreflect.finset]
partition_normedTI [in mathcomp.solvable.frobenius]
partition_class_support [in mathcomp.solvable.frobenius]
partition_big [in mathcomp.ssreflect.bigop]
partition_big_idem [in mathcomp.ssreflect.bigop]
partition0 [in mathcomp.ssreflect.finset]
partnC [in mathcomp.ssreflect.prime]
partnI [in mathcomp.ssreflect.prime]
partnM [in mathcomp.ssreflect.prime]
partnNK [in mathcomp.ssreflect.prime]
partnT [in mathcomp.ssreflect.prime]
partnX [in mathcomp.ssreflect.prime]
partn_part [in mathcomp.ssreflect.prime]
partn_eq1 [in mathcomp.ssreflect.prime]
partn_biggcd [in mathcomp.ssreflect.prime]
partn_biglcm [in mathcomp.ssreflect.prime]
partn_gcd [in mathcomp.ssreflect.prime]
partn_lcm [in mathcomp.ssreflect.prime]
partn_pi [in mathcomp.ssreflect.prime]
partn_dvd [in mathcomp.ssreflect.prime]
partn_exponentS [in mathcomp.solvable.abelian]
partn0 [in mathcomp.ssreflect.prime]
partn1 [in mathcomp.ssreflect.prime]
part_p'nat [in mathcomp.ssreflect.prime]
part_pnat_id [in mathcomp.ssreflect.prime]
part_pnat [in mathcomp.ssreflect.prime]
part_gt0 [in mathcomp.ssreflect.prime]
Pascal [in mathcomp.ssreflect.binomial]
pathP [in mathcomp.ssreflect.path]
path_map [in mathcomp.ssreflect.path]
path_filter [in mathcomp.ssreflect.path]
path_mask [in mathcomp.ssreflect.path]
path_pairwise [in mathcomp.ssreflect.path]
path_sortedE [in mathcomp.ssreflect.path]
path_le [in mathcomp.ssreflect.path]
path_filter_in [in mathcomp.ssreflect.path]
path_mask_in [in mathcomp.ssreflect.path]
path_pairwise_in [in mathcomp.ssreflect.path]
path_sorted_inE [in mathcomp.ssreflect.path]
path_relI [in mathcomp.ssreflect.path]
path_min_sorted [in mathcomp.ssreflect.path]
path_sorted [in mathcomp.ssreflect.path]
path_connect [in mathcomp.ssreflect.fingraph]
pblockK [in mathcomp.ssreflect.finset]
pblock_transversal [in mathcomp.ssreflect.finset]
pblock_inj [in mathcomp.ssreflect.finset]
pblock_equivalence [in mathcomp.ssreflect.finset]
pblock_equivalence_partition [in mathcomp.ssreflect.finset]
pblock_mem [in mathcomp.ssreflect.finset]
PCanHasChoice [in mathcomp.ssreflect.choice]
pcan_pickleK [in mathcomp.ssreflect.choice]
pcan_in_comp [in mathcomp.ssreflect.ssrbool]
pcan_in_inj [in mathcomp.ssreflect.ssrbool]
pcan_enumP [in mathcomp.ssreflect.fintype]
pcoreI [in mathcomp.solvable.pgroup]
pcoreJ [in mathcomp.solvable.pgroup]
pcoreNK [in mathcomp.solvable.pgroup]
pcoreS [in mathcomp.solvable.pgroup]
pcore_faithful_mx_irr [in mathcomp.character.mxabelem]
pcore_sub_rker_mx_irr [in mathcomp.character.mxabelem]
pcore_sub_rstab_mxsimple [in mathcomp.character.mxabelem]
pcore_faithful_irr_act [in mathcomp.solvable.sylow]
pcore_sub_astab_irr [in mathcomp.solvable.sylow]
pcore_setI_normal [in mathcomp.solvable.pgroup]
pcore_modp [in mathcomp.solvable.pgroup]
pcore_mod1 [in mathcomp.solvable.pgroup]
pcore_mod_res [in mathcomp.solvable.pgroup]
pcore_mod_sub [in mathcomp.solvable.pgroup]
pcore_char [in mathcomp.solvable.pgroup]
pcore_normal [in mathcomp.solvable.pgroup]
pcore_pgroup_id [in mathcomp.solvable.pgroup]
pcore_max [in mathcomp.solvable.pgroup]
pcore_sub_Hall [in mathcomp.solvable.pgroup]
pcore_sub [in mathcomp.solvable.pgroup]
pcore_pgroup [in mathcomp.solvable.pgroup]
pcore_psubgroup [in mathcomp.solvable.pgroup]
pcore_Fitting [in mathcomp.solvable.maximal]
Pdeg2.FieldMonic.deg2_poly_root2 [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_root1 [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_factor [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_canonical [in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_root2 [in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_root1 [in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_factor [in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_canonical [in mathcomp.algebra.poly]
pdivP [in mathcomp.ssreflect.prime]
pdiv_pfactor [in mathcomp.ssreflect.prime]
pdiv_id [in mathcomp.ssreflect.prime]
pdiv_min_dvd [in mathcomp.ssreflect.prime]
pdiv_gt0 [in mathcomp.ssreflect.prime]
pdiv_leq [in mathcomp.ssreflect.prime]
pdiv_dvd [in mathcomp.ssreflect.prime]
pdiv_prime [in mathcomp.ssreflect.prime]
pdiv_p_elt [in mathcomp.solvable.abelian]
Pdiv.ClosedField.coprimepP [in mathcomp.algebra.polydiv]
Pdiv.ClosedField.root_coprimep [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Bezoutp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Bezout_coprimepPn [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Bezout_coprimepP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepMl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepMr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepPn [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepX [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepZl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepZr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_XsubC2 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_XsubC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_addl_mul [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_comp_poly [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_gdco [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_div_gcd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_expr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_expl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_pexpr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_pexpl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_root [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_modr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_modl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_dvdr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_dvdl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_sym [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_def [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_size_gcd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprime0p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprime1p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divpN0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp_eq0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp_dvd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp_small [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.div0p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpNl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpNr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpN0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpZl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpZr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_prod_XsubC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul_XsubC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_comp_poly [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gdco [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_pexp2r [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_div_eq0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcd_idr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcd_idl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcdr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcdl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcdlr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_size_eqp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_eqp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_XsubCl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp_sub [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp2r [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_Pexp2l [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp2l [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul2l [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul2r [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mulIr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mulIl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_trans [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mod [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_sub [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_subl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_subr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_add_eq [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_add [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_addl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_addr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mulr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mull [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_leq [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdUp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd_eqp_divl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd0p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd0pP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd1p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdpE [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdpP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdp_recP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqpP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqpxx [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_monic [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_coprimepl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_coprimepr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rgcd_gcd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_gcd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_gcdl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_gcdr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rdiv_div [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rmod_mod [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_root [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_exp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mulr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mull [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mul2l [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mul2r [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_dvdl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_dvdr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_size [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_scale [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rtrans [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_ltrans [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_trans [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_sym [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_eq [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_div_XsubC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp01 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eq_dvdp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_gcdpl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_gcdpr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_dvdp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_dvdpr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_dvdpl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdpC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdpE [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdpp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_comp_poly [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mul2r [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mul2l [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_eqp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_def [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_modr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_modl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_eq0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_exp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_scaler [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_scalel [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mulr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mull [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_addr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_addl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_addl_mul [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcd0p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcd1p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcopP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcop_recP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcop0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gtNdvdp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irredp_XsubCP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irredp_XsubC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irredp_neq0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_gcdpr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_gcdpl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_divpl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_modp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_divpr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_divp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_divpr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_modpN0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_divpl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_modp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modpC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modpp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_XsubC [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_coprime [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_eq0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_eq0P [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_id [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_mulr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_mull [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_small [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.mod0p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.mulp_gcdl [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.mulp_gcdr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.polyC_eqp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.polyXsubCP [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.polyXsubC_eqp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.rcoprimep_coprimep [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_gdco [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_biggcd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_gcd [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_bigmul [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_factor_theorem [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.scalp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_gcdp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_gcd1p [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_poly_eq1 [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_divp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size2_dvdp_gdco [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.uniq_roots_dvdp [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.comm_redivpP [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.leq_rmodp [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.leq_rdivp [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.ltn_rmodpN0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.ltn_rmodp [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.Nrdvdp_small [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdivp_small [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdivp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdiv0p [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdpN0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdp_leq [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvd0p [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvd0pP [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvd1p [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp_def [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp_key [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgcdpE [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgcdp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgcd0p [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgdcop0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodpC [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodpp [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp_eq0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp_eq0P [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp_small [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp0 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp1 [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmod0p [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rscalp_small [in mathcomp.algebra.polydiv]
Pdiv.ComRing.rdivp_eq [in mathcomp.algebra.polydiv]
Pdiv.ComRing.rdvdp_eq [in mathcomp.algebra.polydiv]
Pdiv.ComRing.rdvdp_eqP [in mathcomp.algebra.polydiv]
Pdiv.ComRing.redivpP [in mathcomp.algebra.polydiv]
Pdiv.Field.Bezout_eq1_coprimepP [in mathcomp.algebra.polydiv]
Pdiv.Field.coprimep_map [in mathcomp.algebra.polydiv]
Pdiv.Field.cubic_irreducible [in mathcomp.algebra.polydiv]
Pdiv.Field.divpAC [in mathcomp.algebra.polydiv]
Pdiv.Field.divpD [in mathcomp.algebra.polydiv]
Pdiv.Field.divpE [in mathcomp.algebra.polydiv]
Pdiv.Field.divpK [in mathcomp.algebra.polydiv]
Pdiv.Field.divpKC [in mathcomp.algebra.polydiv]
Pdiv.Field.divpN [in mathcomp.algebra.polydiv]
Pdiv.Field.divpp [in mathcomp.algebra.polydiv]
Pdiv.Field.divpP [in mathcomp.algebra.polydiv]
Pdiv.Field.divpZl [in mathcomp.algebra.polydiv]
Pdiv.Field.divpZr [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_divl [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_pmul2r [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_pmul2l [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_mulCA [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_mulAC [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_mulA [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_addl_mul [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_addl_mul_small [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_modpP [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_eq [in mathcomp.algebra.polydiv]
Pdiv.Field.dvdpE [in mathcomp.algebra.polydiv]
Pdiv.Field.dvdpP [in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_map [in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_gdcor [in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_eq_mul [in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_eq_div [in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_eq [in mathcomp.algebra.polydiv]
Pdiv.Field.edivpP [in mathcomp.algebra.polydiv]
Pdiv.Field.edivp_map [in mathcomp.algebra.polydiv]
Pdiv.Field.edivp_eq [in mathcomp.algebra.polydiv]
Pdiv.Field.edivp_def [in mathcomp.algebra.polydiv]
Pdiv.Field.egcdp_map [in mathcomp.algebra.polydiv]
Pdiv.Field.eqpfP [in mathcomp.algebra.polydiv]
Pdiv.Field.eqpf_eq [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_map [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_rgdco_gdco [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_gdcol [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_gdcor [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_div [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_divr [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_mod [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_modpr [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_divl [in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_modpl [in mathcomp.algebra.polydiv]
Pdiv.Field.expp_sub [in mathcomp.algebra.polydiv]
Pdiv.Field.gcdp_map [in mathcomp.algebra.polydiv]
Pdiv.Field.gdcop_map [in mathcomp.algebra.polydiv]
Pdiv.Field.gdcop_rec_map [in mathcomp.algebra.polydiv]
Pdiv.Field.leq_trunc_divp [in mathcomp.algebra.polydiv]
Pdiv.Field.map_modp [in mathcomp.algebra.polydiv]
Pdiv.Field.map_divp [in mathcomp.algebra.polydiv]
Pdiv.Field.modNp [in mathcomp.algebra.polydiv]
Pdiv.Field.modpD [in mathcomp.algebra.polydiv]
Pdiv.Field.modpE [in mathcomp.algebra.polydiv]
Pdiv.Field.modpN [in mathcomp.algebra.polydiv]
Pdiv.Field.modpP [in mathcomp.algebra.polydiv]
Pdiv.Field.modpZl [in mathcomp.algebra.polydiv]
Pdiv.Field.modpZr [in mathcomp.algebra.polydiv]
Pdiv.Field.modp_mul [in mathcomp.algebra.polydiv]
Pdiv.Field.modp_addl_mul_small [in mathcomp.algebra.polydiv]
Pdiv.Field.mulKp [in mathcomp.algebra.polydiv]
Pdiv.Field.mulpK [in mathcomp.algebra.polydiv]
Pdiv.Field.redivp_map [in mathcomp.algebra.polydiv]
Pdiv.Field.reducible_cubic_root [in mathcomp.algebra.polydiv]
Pdiv.Field.scalpE [in mathcomp.algebra.polydiv]
Pdiv.Field.scalp_map [in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.edivp_key [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.divpE [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.divpp [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.divp_eq [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.drop_poly_divp [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.dvdpP [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.dvdp_eq [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.modpE [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.mulKp [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.mulpK [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.scalpE [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.take_poly_modp [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpAC [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpD [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpK [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpKC [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpN [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpp [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpP [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpZl [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpZr [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_divl [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_pmul2r [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_pmul2l [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_mulCA [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_mulAC [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_mulA [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_addl_mul [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_addl_mul_small [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_eq [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdpP [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdp_eq_mul [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdp_eq_div [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdp_eq [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.edivpP [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.eqp_divl [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.eqp_modpl [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.expp_sub [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.leq_trunc_divp [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpD [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpN [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpP [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpZl [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpZr [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_mul [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_addl_mul_small [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.mulKp [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.mulpK [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.ucl_eqp_eq [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.ulc_eqpP [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.eq_rdvdp [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdivpK [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdivpp [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdivp_eq [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdvdpp [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdvdp_mull [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdvdp_eqP [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.redivp_eq [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rmodpp [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rmodp_mull [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.drop_poly_rdivp [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.eq_rdvdp [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpDl [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpDr [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpK [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpp [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_mull [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_addl_mul [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_addl_mul_small [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_eq [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdvdpP [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdvdpp [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdvdp_mull [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.redivp_eq [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpB [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpD [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpN [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpp [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpX [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpZ [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_compr [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mulml [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mulmr [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_sum [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_id [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_addl_mul_small [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mull [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.take_poly_rmodp [in mathcomp.algebra.polydiv]
Pdiv.Ring.polyXsubCP [in mathcomp.algebra.polydiv]
Pdiv.Ring.rdivp1 [in mathcomp.algebra.polydiv]
Pdiv.Ring.rdvdp_XsubCl [in mathcomp.algebra.polydiv]
Pdiv.Ring.root_factor_theorem [in mathcomp.algebra.polydiv]
Pdiv.UnitRing.uniq_roots_rdvdp [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpE [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpK [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpKC [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpp [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divp_eq [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.dvdpE [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.dvdpP [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.dvdp_eq [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivpP [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivp_eq [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivp_redivp [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivp_def [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.lc_expn_scalp_neq0 [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.modpE [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.mulKp [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.mulpK [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.scalpE [in mathcomp.algebra.polydiv]
pElemI [in mathcomp.solvable.abelian]
pElemJ [in mathcomp.solvable.abelian]
pElemP [in mathcomp.solvable.abelian]
pElemS [in mathcomp.solvable.abelian]
permE [in mathcomp.fingroup.perm]
permEl [in mathcomp.ssreflect.seq]
permJ [in mathcomp.fingroup.perm]
permK [in mathcomp.fingroup.perm]
permKV [in mathcomp.fingroup.perm]
permM [in mathcomp.fingroup.perm]
permP [in mathcomp.fingroup.perm]
permP [in mathcomp.ssreflect.seq]
permPl [in mathcomp.ssreflect.seq]
permPr [in mathcomp.ssreflect.seq]
permS0 [in mathcomp.fingroup.perm]
permS01 [in mathcomp.fingroup.perm]
permS1 [in mathcomp.fingroup.perm]
permutationsE [in mathcomp.ssreflect.seq]
permutationsErot [in mathcomp.ssreflect.seq]
permutations_all_uniq [in mathcomp.ssreflect.seq]
permutations_uniq [in mathcomp.ssreflect.seq]
permX [in mathcomp.fingroup.perm]
permX_fix [in mathcomp.fingroup.perm]
perm_onC [in mathcomp.fingroup.perm]
perm_on_id [in mathcomp.fingroup.perm]
perm_onV [in mathcomp.fingroup.perm]
perm_onM [in mathcomp.fingroup.perm]
perm_on1 [in mathcomp.fingroup.perm]
perm_closed [in mathcomp.fingroup.perm]
perm_mulP [in mathcomp.fingroup.perm]
perm_invP [in mathcomp.fingroup.perm]
perm_oneP [in mathcomp.fingroup.perm]
perm_invK [in mathcomp.fingroup.perm]
perm_onto [in mathcomp.fingroup.perm]
perm_inj [in mathcomp.fingroup.perm]
perm_proof [in mathcomp.fingroup.perm]
perm_permutations [in mathcomp.ssreflect.seq]
perm_count_undup [in mathcomp.ssreflect.seq]
perm_tally_seq [in mathcomp.ssreflect.seq]
perm_tally [in mathcomp.ssreflect.seq]
perm_allpairs [in mathcomp.ssreflect.seq]
perm_allpairs_consr [in mathcomp.ssreflect.seq]
perm_allpairs_catr [in mathcomp.ssreflect.seq]
perm_allpairs_dep [in mathcomp.ssreflect.seq]
perm_flatten [in mathcomp.ssreflect.seq]
perm_zip2 [in mathcomp.ssreflect.seq]
perm_zip1 [in mathcomp.ssreflect.seq]
perm_zip_sym [in mathcomp.ssreflect.seq]
perm_sumn [in mathcomp.ssreflect.seq]
perm_iotaP [in mathcomp.ssreflect.seq]
perm_pmap [in mathcomp.ssreflect.seq]
perm_map_inj [in mathcomp.ssreflect.seq]
perm_map [in mathcomp.ssreflect.seq]
perm_to_subseq [in mathcomp.ssreflect.seq]
perm_to_rem [in mathcomp.ssreflect.seq]
perm_undup [in mathcomp.ssreflect.seq]
perm_uniq [in mathcomp.ssreflect.seq]
perm_small_eq [in mathcomp.ssreflect.seq]
perm_all [in mathcomp.ssreflect.seq]
perm_has [in mathcomp.ssreflect.seq]
perm_consP [in mathcomp.ssreflect.seq]
perm_nilP [in mathcomp.ssreflect.seq]
perm_mem [in mathcomp.ssreflect.seq]
perm_size [in mathcomp.ssreflect.seq]
perm_filterC [in mathcomp.ssreflect.seq]
perm_filter [in mathcomp.ssreflect.seq]
perm_rev [in mathcomp.ssreflect.seq]
perm_rotr [in mathcomp.ssreflect.seq]
perm_rot [in mathcomp.ssreflect.seq]
perm_rcons [in mathcomp.ssreflect.seq]
perm_catACA [in mathcomp.ssreflect.seq]
perm_catCA [in mathcomp.ssreflect.seq]
perm_catAC [in mathcomp.ssreflect.seq]
perm_cat [in mathcomp.ssreflect.seq]
perm_catr [in mathcomp.ssreflect.seq]
perm_cat2r [in mathcomp.ssreflect.seq]
perm_cons [in mathcomp.ssreflect.seq]
perm_catl [in mathcomp.ssreflect.seq]
perm_cat2l [in mathcomp.ssreflect.seq]
perm_catC [in mathcomp.ssreflect.seq]
perm_trans [in mathcomp.ssreflect.seq]
perm_sym [in mathcomp.ssreflect.seq]
perm_refl [in mathcomp.ssreflect.seq]
perm_mxV [in mathcomp.algebra.matrix]
perm_mx_is_perm [in mathcomp.algebra.matrix]
perm_mxM [in mathcomp.algebra.matrix]
perm_mx1 [in mathcomp.algebra.matrix]
perm_mxEsub [in mathcomp.algebra.matrix]
perm_inE [in mathcomp.fingroup.automorphism]
perm_in_on [in mathcomp.fingroup.automorphism]
perm_in_inj [in mathcomp.fingroup.automorphism]
perm_faithful [in mathcomp.fingroup.action]
perm_act1P [in mathcomp.fingroup.action]
perm_mact [in mathcomp.fingroup.action]
perm_sort_inP [in mathcomp.ssreflect.path]
perm_sortP [in mathcomp.ssreflect.path]
perm_iota_sort [in mathcomp.ssreflect.path]
perm_sort [in mathcomp.ssreflect.path]
perm_merge [in mathcomp.ssreflect.path]
perm_bigcprod [in mathcomp.fingroup.gproduct]
perm_basis [in mathcomp.algebra.vector]
perm_free [in mathcomp.algebra.vector]
perm_big_supp [in mathcomp.ssreflect.bigop]
perm_big_supp_cond [in mathcomp.ssreflect.bigop]
perm_big [in mathcomp.ssreflect.bigop]
perm1 [in mathcomp.fingroup.perm]
pexpIrz [in mathcomp.algebra.ssrint]
pexprz_eq1 [in mathcomp.algebra.ssrint]
Pextraspecial.actP [in mathcomp.solvable.extraspecial]
Pextraspecial.gactP [in mathcomp.solvable.extraspecial]
Pextraspecial.gtype_key [in mathcomp.solvable.extraspecial]
pfactorK [in mathcomp.ssreflect.prime]
pfactorKpdiv [in mathcomp.ssreflect.prime]
pfactor_coprime [in mathcomp.ssreflect.prime]
pfactor_dvdnn [in mathcomp.ssreflect.prime]
pfactor_dvdn [in mathcomp.ssreflect.prime]
pfactor_gt0 [in mathcomp.ssreflect.prime]
pfamilyP [in mathcomp.ssreflect.finfun]
pffun_onP [in mathcomp.ssreflect.finfun]
pgroupE [in mathcomp.solvable.pgroup]
pgroupJ [in mathcomp.solvable.pgroup]
pgroupM [in mathcomp.solvable.pgroup]
pgroupNK [in mathcomp.solvable.pgroup]
pgroupP [in mathcomp.solvable.pgroup]
pgroupS [in mathcomp.solvable.pgroup]
pgroup_sol [in mathcomp.solvable.sylow]
pgroup_nil [in mathcomp.solvable.sylow]
pgroup_fix_mod [in mathcomp.solvable.sylow]
pgroup_pdiv [in mathcomp.solvable.pgroup]
pgroup_p [in mathcomp.solvable.pgroup]
pgroup_pi [in mathcomp.solvable.pgroup]
pgroup_cyclic_faithful [in mathcomp.character.character]
pgroup1 [in mathcomp.solvable.pgroup]
pHallE [in mathcomp.solvable.pgroup]
pHallJ [in mathcomp.solvable.pgroup]
pHallJnorm [in mathcomp.solvable.pgroup]
pHallJ2 [in mathcomp.solvable.pgroup]
pHallNK [in mathcomp.solvable.pgroup]
pHallP [in mathcomp.solvable.pgroup]
pHall_id [in mathcomp.solvable.pgroup]
pHall_subl [in mathcomp.solvable.pgroup]
pHall_Hall [in mathcomp.solvable.pgroup]
pHall_pgroup [in mathcomp.solvable.pgroup]
pHall_sub [in mathcomp.solvable.pgroup]
PhiJ [in mathcomp.solvable.maximal]
PhiS [in mathcomp.solvable.maximal]
Phi_mulg [in mathcomp.solvable.maximal]
Phi_cprod [in mathcomp.solvable.maximal]
Phi_min [in mathcomp.solvable.maximal]
Phi_Mho [in mathcomp.solvable.maximal]
Phi_joing [in mathcomp.solvable.maximal]
Phi_quotient_abelem [in mathcomp.solvable.maximal]
Phi_quotient_cyclic [in mathcomp.solvable.maximal]
Phi_quotient_id [in mathcomp.solvable.maximal]
Phi_normal [in mathcomp.solvable.maximal]
Phi_char [in mathcomp.solvable.maximal]
Phi_nongen [in mathcomp.solvable.maximal]
Phi_proper [in mathcomp.solvable.maximal]
Phi_sub_max [in mathcomp.solvable.maximal]
Phi_sub [in mathcomp.solvable.maximal]
pickleK_inv [in mathcomp.ssreflect.choice]
pickle_taggedK [in mathcomp.ssreflect.choice]
pickle_seqK [in mathcomp.ssreflect.choice]
pickle_invK [in mathcomp.ssreflect.choice]
pickP [in mathcomp.ssreflect.fintype]
pid_mxEcol [in mathcomp.algebra.matrix]
pid_mxErow [in mathcomp.algebra.matrix]
pid_mx_id [in mathcomp.algebra.matrix]
pid_mx_minh [in mathcomp.algebra.matrix]
pid_mx_minv [in mathcomp.algebra.matrix]
pid_mx_block [in mathcomp.algebra.matrix]
pid_mx_col [in mathcomp.algebra.matrix]
pid_mx_row [in mathcomp.algebra.matrix]
pid_mx_1 [in mathcomp.algebra.matrix]
pid_mx_0 [in mathcomp.algebra.matrix]
pid_mx_key [in mathcomp.algebra.matrix]
pinvmxE [in mathcomp.algebra.mxalgebra]
pinvmx_full [in mathcomp.algebra.mxalgebra]
pinvmx_free [in mathcomp.algebra.mxalgebra]
piOhm1 [in mathcomp.solvable.abelian]
piP [in mathcomp.ssreflect.generic_quotient]
piSg [in mathcomp.fingroup.fingroup]
pi_morph11 [in mathcomp.ssreflect.generic_quotient]
pi_mono2 [in mathcomp.ssreflect.generic_quotient]
pi_mono1 [in mathcomp.ssreflect.generic_quotient]
pi_morph2 [in mathcomp.ssreflect.generic_quotient]
pi_morph1 [in mathcomp.ssreflect.generic_quotient]
pi_subfext_inv [in mathcomp.field.fieldext]
pi_subfext_mul [in mathcomp.field.fieldext]
pi_subfext_opp [in mathcomp.field.fieldext]
pi_subfext_add [in mathcomp.field.fieldext]
pi_subfx_inj [in mathcomp.field.fieldext]
pi_is_multiplicative [in mathcomp.algebra.ring_quotient]
pi_is_additive [in mathcomp.algebra.ring_quotient]
pi_center_nilpotent [in mathcomp.solvable.sylow]
pi_p'group [in mathcomp.solvable.pgroup]
pi_pgroup [in mathcomp.solvable.pgroup]
pi_p'nat [in mathcomp.ssreflect.prime]
pi_pnat [in mathcomp.ssreflect.prime]
pi_of_prime [in mathcomp.ssreflect.prime]
pi_of_exp [in mathcomp.ssreflect.prime]
pi_of_part [in mathcomp.ssreflect.prime]
pi_ofM [in mathcomp.ssreflect.prime]
pi_of_dvd [in mathcomp.ssreflect.prime]
pi_max_pdiv [in mathcomp.ssreflect.prime]
pi_pdiv [in mathcomp.ssreflect.prime]
pi_of_exponent [in mathcomp.solvable.abelian]
pi'_p'group [in mathcomp.solvable.pgroup]
pi'_p'nat [in mathcomp.ssreflect.prime]
plogpD [in mathcomp.field.qfpoly]
plogp_div_eq0 [in mathcomp.field.qfpoly]
plogp_X [in mathcomp.field.qfpoly]
plogp_lt [in mathcomp.field.qfpoly]
plogp0 [in mathcomp.field.qfpoly]
plogp1 [in mathcomp.field.qfpoly]
plusE [in mathcomp.ssreflect.ssrnat]
pmapS_filter [in mathcomp.ssreflect.seq]
pmap_sub_uniq [in mathcomp.ssreflect.seq]
pmap_uniq [in mathcomp.ssreflect.seq]
pmap_cat [in mathcomp.ssreflect.seq]
pmap_filter [in mathcomp.ssreflect.seq]
pmaxElemJ [in mathcomp.solvable.abelian]
pmaxElemP [in mathcomp.solvable.abelian]
pmaxElemS [in mathcomp.solvable.abelian]
pmaxElem_LdivP [in mathcomp.solvable.abelian]
pmaxElem_exists [in mathcomp.solvable.abelian]
pmaxElem_extraspecial [in mathcomp.solvable.maximal]
pmorphimF [in mathcomp.solvable.gfunctor]
pmorphim_pHall [in mathcomp.solvable.pgroup]
pmorphim_pgroup [in mathcomp.solvable.pgroup]
pmulrn [in mathcomp.algebra.ssrint]
pmulrz_rle0 [in mathcomp.algebra.ssrint]
pmulrz_rge0 [in mathcomp.algebra.ssrint]
pmulrz_rlt0 [in mathcomp.algebra.ssrint]
pmulrz_rgt0 [in mathcomp.algebra.ssrint]
pmulrz_lle0 [in mathcomp.algebra.ssrint]
pmulrz_lge0 [in mathcomp.algebra.ssrint]
pmulrz_llt0 [in mathcomp.algebra.ssrint]
pmulrz_lgt0 [in mathcomp.algebra.ssrint]
pnatE [in mathcomp.ssreflect.prime]
pnatI [in mathcomp.ssreflect.prime]
pnatM [in mathcomp.ssreflect.prime]
pnatNK [in mathcomp.ssreflect.prime]
pnatP [in mathcomp.ssreflect.prime]
pnatPpi [in mathcomp.ssreflect.prime]
pnatX [in mathcomp.ssreflect.prime]
pnat_1 [in mathcomp.ssreflect.prime]
pnat_coprime [in mathcomp.ssreflect.prime]
pnat_div [in mathcomp.ssreflect.prime]
pnat_dvd [in mathcomp.ssreflect.prime]
pnat_pi [in mathcomp.ssreflect.prime]
pnat_id [in mathcomp.ssreflect.prime]
pnat_exponent [in mathcomp.solvable.abelian]
pnElemE [in mathcomp.solvable.abelian]
pnElemI [in mathcomp.solvable.abelian]
pnElemJ [in mathcomp.solvable.abelian]
pnElemP [in mathcomp.solvable.abelian]
pnElemPcard [in mathcomp.solvable.abelian]
pnElemS [in mathcomp.solvable.abelian]
pnElem_prime [in mathcomp.solvable.abelian]
pnElem0 [in mathcomp.solvable.abelian]
polyCB [in mathcomp.algebra.poly]
polyCD [in mathcomp.algebra.poly]
polyCK [in mathcomp.algebra.poly]
polyCM [in mathcomp.algebra.poly]
polyCMn [in mathcomp.algebra.poly]
polyCMz [in mathcomp.algebra.ssrint]
polyCN [in mathcomp.algebra.poly]
polyCV [in mathcomp.algebra.poly]
polyC_natr [in mathcomp.algebra.poly]
polyC_exp [in mathcomp.algebra.poly]
polyC_multiplicative [in mathcomp.algebra.poly]
polyC_eq0 [in mathcomp.algebra.poly]
polyC_inj [in mathcomp.algebra.poly]
polyC0 [in mathcomp.algebra.poly]
polyC1 [in mathcomp.algebra.poly]
PolyK [in mathcomp.algebra.poly]
polyn_is_linear [in mathcomp.algebra.qpoly]
polyOverC [in mathcomp.algebra.poly]
polyOverNr [in mathcomp.algebra.poly]
polyOverP [in mathcomp.algebra.poly]
polyOverS [in mathcomp.algebra.poly]
polyOverSv [in mathcomp.field.fieldext]
polyOverX [in mathcomp.algebra.poly]
polyOverXsubC [in mathcomp.algebra.poly]
polyOverZ [in mathcomp.algebra.poly]
polyOver_dvdzP [in mathcomp.algebra.intdiv]
polyOver_subvs [in mathcomp.field.fieldext]
polyOver_comp [in mathcomp.algebra.poly]
polyOver_nderivn [in mathcomp.algebra.poly]
polyOver_derivn [in mathcomp.algebra.poly]
polyOver_deriv [in mathcomp.algebra.poly]
polyOver_mul1_closed [in mathcomp.algebra.poly]
polyOver_mulr_2closed [in mathcomp.algebra.poly]
polyOver_addr_closed [in mathcomp.algebra.poly]
polyOver_poly [in mathcomp.algebra.poly]
polyOver0 [in mathcomp.algebra.poly]
polyOver1P [in mathcomp.field.falgebra]
polyP [in mathcomp.algebra.poly]
polyseqC [in mathcomp.algebra.poly]
polyseqK [in mathcomp.algebra.poly]
polyseqMX [in mathcomp.algebra.poly]
polyseqMXn [in mathcomp.algebra.poly]
polyseqX [in mathcomp.algebra.poly]
polyseqXn [in mathcomp.algebra.poly]
polyseqXsubC [in mathcomp.algebra.poly]
polyseq_poly [in mathcomp.algebra.poly]
polyseq_cons [in mathcomp.algebra.poly]
polyseq0 [in mathcomp.algebra.poly]
polyseq1 [in mathcomp.algebra.poly]
polySpred [in mathcomp.algebra.poly]
polyXsubC_eq0 [in mathcomp.algebra.poly]
polyX_eq0 [in mathcomp.algebra.poly]
polyX_key [in mathcomp.algebra.poly]
poly_square_freeP [in mathcomp.field.separable]
poly_rV_is_linear [in mathcomp.algebra.mxpoly]
poly_rV_K [in mathcomp.algebra.mxpoly]
poly_XmY_eq0 [in mathcomp.algebra.polyXY]
poly_XaY_eq0 [in mathcomp.algebra.polyXY]
poly_XmY0 [in mathcomp.algebra.polyXY]
poly_XaY0 [in mathcomp.algebra.polyXY]
poly_invE [in mathcomp.algebra.poly]
poly_unitE [in mathcomp.algebra.poly]
poly_inv_out [in mathcomp.algebra.poly]
poly_intro_unit [in mathcomp.algebra.poly]
poly_mulVp [in mathcomp.algebra.poly]
poly_idomainAxiom [in mathcomp.algebra.poly]
poly_alg_initial [in mathcomp.algebra.poly]
poly_mul_comm [in mathcomp.algebra.poly]
poly_take_drop [in mathcomp.algebra.poly]
poly_even_odd [in mathcomp.algebra.poly]
poly_initial [in mathcomp.algebra.poly]
poly_morphX_comm [in mathcomp.algebra.poly]
poly_def [in mathcomp.algebra.poly]
poly_ind [in mathcomp.algebra.poly]
poly_key [in mathcomp.algebra.poly]
poly_inj [in mathcomp.algebra.poly]
poly_of_qpolyZ [in mathcomp.algebra.qpoly]
poly_of_qpolyX [in mathcomp.algebra.qpoly]
poly_of_qpolyM [in mathcomp.algebra.qpoly]
poly_of_qpolyD [in mathcomp.algebra.qpoly]
poly_of_qpoly_sum [in mathcomp.algebra.qpoly]
poly_of_size_mod [in mathcomp.algebra.qpoly]
poly0Vpos [in mathcomp.algebra.poly]
poly1_neq0 [in mathcomp.algebra.poly]
poly2_root [in mathcomp.algebra.poly]
porbitE [in mathcomp.fingroup.action]
porbitP [in mathcomp.fingroup.perm]
porbitPmin [in mathcomp.fingroup.perm]
porbitsV [in mathcomp.fingroup.perm]
porbits_mul_tperm [in mathcomp.fingroup.perm]
porbitV [in mathcomp.fingroup.perm]
porbit_setP [in mathcomp.fingroup.perm]
porbit_perm [in mathcomp.fingroup.perm]
porbit_sym [in mathcomp.fingroup.perm]
porbit_traject [in mathcomp.fingroup.perm]
porbit_id [in mathcomp.fingroup.perm]
porbit_actperm [in mathcomp.fingroup.action]
posnP [in mathcomp.ssreflect.ssrnat]
PoszD [in mathcomp.algebra.ssrint]
PoszM [in mathcomp.algebra.ssrint]
powersetCE [in mathcomp.ssreflect.finset]
powersetE [in mathcomp.ssreflect.finset]
powersetI [in mathcomp.ssreflect.finset]
powersetS [in mathcomp.ssreflect.finset]
powersetT [in mathcomp.ssreflect.finset]
powerset0 [in mathcomp.ssreflect.finset]
powerset1 [in mathcomp.ssreflect.finset]
powX_eq_mod [in mathcomp.field.qfpoly]
pprodE [in mathcomp.fingroup.gproduct]
pprodEY [in mathcomp.fingroup.gproduct]
pprodg1 [in mathcomp.fingroup.gproduct]
pprodJ [in mathcomp.fingroup.gproduct]
pprodmE [in mathcomp.fingroup.gproduct]
pprodmEl [in mathcomp.fingroup.gproduct]
pprodmEr [in mathcomp.fingroup.gproduct]
pprodmM [in mathcomp.fingroup.gproduct]
pprodP [in mathcomp.fingroup.gproduct]
pprodW [in mathcomp.fingroup.gproduct]
pprodWC [in mathcomp.fingroup.gproduct]
pprodWY [in mathcomp.fingroup.gproduct]
pprod1g [in mathcomp.fingroup.gproduct]
pquotient_pcore [in mathcomp.solvable.pgroup]
pquotient_pHall [in mathcomp.solvable.pgroup]
pquotient_pgroup [in mathcomp.solvable.pgroup]
PreClosedField.closed_nonrootP [in mathcomp.algebra.poly]
PreClosedField.closed_rootP [in mathcomp.algebra.poly]
predC_itv [in mathcomp.algebra.interval]
predC_itvr [in mathcomp.algebra.interval]
predC_itvl [in mathcomp.algebra.interval]
predC_closed [in mathcomp.ssreflect.fingraph]
predD1P [in mathcomp.ssreflect.eqtype]
prednK [in mathcomp.ssreflect.ssrnat]
predn_exp [in mathcomp.ssreflect.binomial]
predn_sub [in mathcomp.ssreflect.ssrnat]
predn_int [in mathcomp.algebra.ssrint]
predT_subset [in mathcomp.ssreflect.fintype]
predU1l [in mathcomp.ssreflect.eqtype]
predU1P [in mathcomp.ssreflect.eqtype]
predU1r [in mathcomp.ssreflect.eqtype]
predX_prod_enum [in mathcomp.ssreflect.fintype]
pred0P [in mathcomp.ssreflect.fintype]
pred0Pn [in mathcomp.ssreflect.fintype]
pred1E [in mathcomp.ssreflect.eqtype]
pred2P [in mathcomp.ssreflect.eqtype]
prefixE [in mathcomp.ssreflect.seq]
prefixP [in mathcomp.ssreflect.seq]
prefixs0 [in mathcomp.ssreflect.seq]
prefixs1 [in mathcomp.ssreflect.seq]
prefixW [in mathcomp.ssreflect.seq]
prefix_index [in mathcomp.ssreflect.seq]
prefix_drop_gt0 [in mathcomp.ssreflect.seq]
prefix_take [in mathcomp.ssreflect.seq]
prefix_uniq [in mathcomp.ssreflect.seq]
prefix_suffix_trans [in mathcomp.ssreflect.seq]
prefix_infix_trans [in mathcomp.ssreflect.seq]
prefix_infix [in mathcomp.ssreflect.seq]
prefix_revLR [in mathcomp.ssreflect.seq]
prefix_rev [in mathcomp.ssreflect.seq]
prefix_rcons [in mathcomp.ssreflect.seq]
prefix_catl [in mathcomp.ssreflect.seq]
prefix_trans [in mathcomp.ssreflect.seq]
prefix_prefix [in mathcomp.ssreflect.seq]
prefix_catr [in mathcomp.ssreflect.seq]
prefix_cons [in mathcomp.ssreflect.seq]
prefix_refl [in mathcomp.ssreflect.seq]
prefix_subseq [in mathcomp.ssreflect.seq]
prefix_sorted [in mathcomp.ssreflect.path]
prefix_path [in mathcomp.ssreflect.path]
prefix0s [in mathcomp.ssreflect.seq]
prefix1s [in mathcomp.ssreflect.seq]
preimsetC [in mathcomp.ssreflect.finset]
preimsetD [in mathcomp.ssreflect.finset]
preimsetI [in mathcomp.ssreflect.finset]
preimsetS [in mathcomp.ssreflect.finset]
preimsetT [in mathcomp.ssreflect.finset]
preimsetU [in mathcomp.ssreflect.finset]
preimset_proper [in mathcomp.ssreflect.finset]
preimset0 [in mathcomp.ssreflect.finset]
preim_permV [in mathcomp.fingroup.perm]
preim_partition_pblock [in mathcomp.ssreflect.finset]
preim_partitionP [in mathcomp.ssreflect.finset]
preim_autE [in mathcomp.fingroup.automorphism]
preim_iinv [in mathcomp.ssreflect.fintype]
prevE [in mathcomp.ssreflect.fingraph]
prev_map [in mathcomp.ssreflect.path]
prev_rev [in mathcomp.ssreflect.path]
prev_rotr [in mathcomp.ssreflect.path]
prev_rot [in mathcomp.ssreflect.path]
prev_next [in mathcomp.ssreflect.path]
prev_cycle [in mathcomp.ssreflect.path]
prev_nth [in mathcomp.ssreflect.path]
pre_image [in mathcomp.ssreflect.fintype]
primeChar_dimf [in mathcomp.field.finfield]
primeChar_vectAxiom [in mathcomp.field.finfield]
primeChar_pgroup [in mathcomp.field.finfield]
primeChar_abelem [in mathcomp.field.finfield]
primeChar_scaleAr [in mathcomp.field.finfield]
primeChar_scaleAl [in mathcomp.field.finfield]
primeChar_scaleDl [in mathcomp.field.finfield]
primeChar_scaleDr [in mathcomp.field.finfield]
primeChar_scale1 [in mathcomp.field.finfield]
primeChar_scaleA [in mathcomp.field.finfield]
PrimeDecompAux.edivn2P [in mathcomp.ssreflect.prime]
PrimeDecompAux.elogn2P [in mathcomp.ssreflect.prime]
PrimeDecompAux.ifnzP [in mathcomp.ssreflect.prime]
primeP [in mathcomp.ssreflect.prime]
primePn [in mathcomp.ssreflect.prime]
primePns [in mathcomp.ssreflect.prime]
PrimePowerField [in mathcomp.field.finfield]
primesM [in mathcomp.ssreflect.prime]
primesX [in mathcomp.ssreflect.prime]
primes_class_simple_gt1 [in mathcomp.character.integral_char]
primes_part [in mathcomp.ssreflect.prime]
primes_prime [in mathcomp.ssreflect.prime]
primes_uniq [in mathcomp.ssreflect.prime]
primes_exponent [in mathcomp.solvable.abelian]
prime_modn_expSn [in mathcomp.ssreflect.binomial]
prime_dvd_bin [in mathcomp.ssreflect.binomial]
prime_idealrM [in mathcomp.algebra.ring_quotient]
prime_invariant_irr_extendible [in mathcomp.character.inertia]
prime_meetG [in mathcomp.fingroup.fingroup]
prime_TIg [in mathcomp.fingroup.fingroup]
prime_subgroupVti [in mathcomp.solvable.pgroup]
prime_FrobeniusP [in mathcomp.solvable.frobenius]
prime_decompE [in mathcomp.ssreflect.prime]
prime_above [in mathcomp.ssreflect.prime]
prime_coprime [in mathcomp.ssreflect.prime]
prime_oddPn [in mathcomp.ssreflect.prime]
prime_gt0 [in mathcomp.ssreflect.prime]
prime_gt1 [in mathcomp.ssreflect.prime]
prime_nt_dvdP [in mathcomp.ssreflect.prime]
prime_decomp_correct [in mathcomp.ssreflect.prime]
prime_Ohm1P [in mathcomp.solvable.extremal]
prime_abelem [in mathcomp.solvable.abelian]
prime_cyclic [in mathcomp.solvable.cyclic]
Primitive_Element_Theorem [in mathcomp.field.separable]
primitive_poly_in_qpoly_eq0 [in mathcomp.field.qfpoly]
primitive_mi [in mathcomp.field.qfpoly]
primitive_polyP [in mathcomp.field.qfpoly]
primitive_root_splitting_abelian [in mathcomp.character.mxrepresentation]
prim_trans_norm [in mathcomp.solvable.primitive_action]
prim_rootP [in mathcomp.algebra.poly]
prim_root_exp_coprime [in mathcomp.algebra.poly]
prim_order_dvd [in mathcomp.algebra.poly]
prim_expr_mod [in mathcomp.algebra.poly]
prim_expr_order [in mathcomp.algebra.poly]
prim_order_gt0 [in mathcomp.algebra.poly]
prim_order_exists [in mathcomp.algebra.poly]
principal_comp_key [in mathcomp.character.mxrepresentation]
principal_comp_subproof [in mathcomp.character.mxrepresentation]
prodMz [in mathcomp.algebra.ssrint]
prodn_gt0 [in mathcomp.ssreflect.bigop]
prodn_cond_gt0 [in mathcomp.ssreflect.bigop]
prodsgP [in mathcomp.fingroup.fingroup]
prodvA [in mathcomp.field.falgebra]
prodvAC [in mathcomp.field.fieldext]
prodvC [in mathcomp.field.fieldext]
prodvCA [in mathcomp.field.fieldext]
prodvDl [in mathcomp.field.falgebra]
prodvDr [in mathcomp.field.falgebra]
prodvP [in mathcomp.field.falgebra]
prodvS [in mathcomp.field.falgebra]
prodvSl [in mathcomp.field.falgebra]
prodvSr [in mathcomp.field.falgebra]
prodv_is_aspace [in mathcomp.field.fieldext]
prodv_sub [in mathcomp.field.falgebra]
prodv_id [in mathcomp.field.falgebra]
prodv_line [in mathcomp.field.falgebra]
prodv_key [in mathcomp.field.falgebra]
prodv0 [in mathcomp.field.falgebra]
prodv1 [in mathcomp.field.falgebra]
prod_tpermP [in mathcomp.fingroup.perm]
prod_Cyclotomic [in mathcomp.field.cyclotomic]
prod_cyclotomic [in mathcomp.field.cyclotomic]
prod_cfunE [in mathcomp.character.classfun]
prod_constt [in mathcomp.solvable.pgroup]
prod_prime_decomp [in mathcomp.ssreflect.prime]
prod_t_correct [in mathcomp.solvable.burnside_app]
prod_repr_lin [in mathcomp.character.character]
prod_mx_repr [in mathcomp.character.character]
prod_enumP [in mathcomp.ssreflect.fintype]
prod_nat_seq_neq1 [in mathcomp.ssreflect.bigop]
prod_nat_seq_eq1 [in mathcomp.ssreflect.bigop]
prod_nat_seq_neq0 [in mathcomp.ssreflect.bigop]
prod_nat_seq_eq0 [in mathcomp.ssreflect.bigop]
prod_nat_const_nat [in mathcomp.ssreflect.bigop]
prod_nat_const [in mathcomp.ssreflect.bigop]
prod0v [in mathcomp.field.falgebra]
prod1v [in mathcomp.field.falgebra]
projv_proj [in mathcomp.algebra.vector]
projv_id [in mathcomp.algebra.vector]
proj_mx_hom [in mathcomp.character.mxrepresentation]
proj_factmodS [in mathcomp.character.mxrepresentation]
proj_mx_proj [in mathcomp.algebra.mxalgebra]
proj_mx_0 [in mathcomp.algebra.mxalgebra]
proj_mx_id [in mathcomp.algebra.mxalgebra]
proj_mx_compl_sub [in mathcomp.algebra.mxalgebra]
proj_mx_sub [in mathcomp.algebra.mxalgebra]
properC [in mathcomp.ssreflect.finset]
properCl [in mathcomp.ssreflect.finset]
properCr [in mathcomp.ssreflect.finset]
properD [in mathcomp.ssreflect.finset]
properD1 [in mathcomp.ssreflect.finset]
properE [in mathcomp.ssreflect.fintype]
properEcard [in mathcomp.ssreflect.finset]
properEneq [in mathcomp.ssreflect.finset]
properG_ltn_log [in mathcomp.solvable.pgroup]
properI [in mathcomp.ssreflect.finset]
properIl [in mathcomp.ssreflect.finset]
properIr [in mathcomp.ssreflect.finset]
properIset [in mathcomp.ssreflect.finset]
properJ [in mathcomp.fingroup.fingroup]
properP [in mathcomp.ssreflect.fintype]
properT [in mathcomp.ssreflect.finset]
properU [in mathcomp.ssreflect.finset]
properUl [in mathcomp.ssreflect.finset]
properUr [in mathcomp.ssreflect.finset]
properxx [in mathcomp.ssreflect.fintype]
proper_neq [in mathcomp.ssreflect.finset]
proper_irrefl [in mathcomp.ssreflect.fintype]
proper_card [in mathcomp.ssreflect.fintype]
proper_sub_trans [in mathcomp.ssreflect.fintype]
proper_trans [in mathcomp.ssreflect.fintype]
proper_subn [in mathcomp.ssreflect.fintype]
proper_sub [in mathcomp.ssreflect.fintype]
proper0 [in mathcomp.ssreflect.finset]
proper1G [in mathcomp.fingroup.fingroup]
proper1set [in mathcomp.ssreflect.finset]
pseriesJ [in mathcomp.solvable.pgroup]
pseriesS [in mathcomp.solvable.pgroup]
pseries_rcons_id [in mathcomp.solvable.pgroup]
pseries_char_catr [in mathcomp.solvable.pgroup]
pseries_catr_id [in mathcomp.solvable.pgroup]
pseries_char_catl [in mathcomp.solvable.pgroup]
pseries_catl_id [in mathcomp.solvable.pgroup]
pseries_sub_catr [in mathcomp.solvable.pgroup]
pseries_norm2 [in mathcomp.solvable.pgroup]
pseries_sub_catl [in mathcomp.solvable.pgroup]
pseries_pop2 [in mathcomp.solvable.pgroup]
pseries_pop [in mathcomp.solvable.pgroup]
pseries_normal [in mathcomp.solvable.pgroup]
pseries_char [in mathcomp.solvable.pgroup]
pseries_sub [in mathcomp.solvable.pgroup]
pseries_subfun [in mathcomp.solvable.pgroup]
pseries_rcons [in mathcomp.solvable.pgroup]
pseries_group_set [in mathcomp.solvable.pgroup]
pseries1 [in mathcomp.solvable.pgroup]
psubgroupJ [in mathcomp.solvable.pgroup]
psubgroup1 [in mathcomp.solvable.pgroup]
purely_inseparable_trans [in mathcomp.field.separable]
purely_inseparable_refl [in mathcomp.field.separable]
purely_inseparableP [in mathcomp.field.separable]
purely_inseparable_elementP [in mathcomp.field.separable]
pvalE [in mathcomp.fingroup.perm]
pX1p2id [in mathcomp.solvable.extraspecial]
pX1p2n_extraspecial [in mathcomp.solvable.extraspecial]
pX1p2n_pgroup [in mathcomp.solvable.extraspecial]
pX1p2S [in mathcomp.solvable.extraspecial]
pX1p2_extraspecial [in mathcomp.solvable.extraspecial]
pX1p2_pgroup [in mathcomp.solvable.extraspecial]
p_elt_constt [in mathcomp.solvable.pgroup]
p_eltNK [in mathcomp.solvable.pgroup]
p_eltJ [in mathcomp.solvable.pgroup]
p_eltX [in mathcomp.solvable.pgroup]
p_eltV [in mathcomp.solvable.pgroup]
p_elt1 [in mathcomp.solvable.pgroup]
p_eltM [in mathcomp.solvable.pgroup]
p_eltM_norm [in mathcomp.solvable.pgroup]
p_elt_exp [in mathcomp.solvable.pgroup]
p_group1 [in mathcomp.solvable.pgroup]
p_Sylow [in mathcomp.solvable.pgroup]
p_groupJ [in mathcomp.solvable.pgroup]
p_groupP [in mathcomp.solvable.pgroup]
p_natP [in mathcomp.ssreflect.prime]
p_part_gt1 [in mathcomp.ssreflect.prime]
p_part_eq1 [in mathcomp.ssreflect.prime]
p_part [in mathcomp.ssreflect.prime]
p_rank_abelian [in mathcomp.solvable.abelian]
p_rank_Ohm1 [in mathcomp.solvable.abelian]
p_rank_p'quotient [in mathcomp.solvable.abelian]
p_rank_dprod [in mathcomp.solvable.abelian]
p_rank_quotient [in mathcomp.solvable.abelian]
p_rank_le_rank [in mathcomp.solvable.abelian]
p_rank_pmaxElem_exists [in mathcomp.solvable.abelian]
p_rank_Hall [in mathcomp.solvable.abelian]
p_rank_Sylow [in mathcomp.solvable.abelian]
p_rankJ [in mathcomp.solvable.abelian]
p_rankElem_max [in mathcomp.solvable.abelian]
p_rankS [in mathcomp.solvable.abelian]
p_rank_abelem [in mathcomp.solvable.abelian]
p_rank_le_logn [in mathcomp.solvable.abelian]
p_rank1 [in mathcomp.solvable.abelian]
p_rank_gt0 [in mathcomp.solvable.abelian]
p_rank_geP [in mathcomp.solvable.abelian]
p_rank_witness [in mathcomp.solvable.abelian]
p_abelem_split1 [in mathcomp.solvable.maximal]
p_core_Fitting [in mathcomp.solvable.maximal]
p_index_maximal [in mathcomp.solvable.maximal]
p_maximal_index [in mathcomp.solvable.maximal]
p_maximal_normal [in mathcomp.solvable.maximal]
p'groupEpi [in mathcomp.solvable.pgroup]
p'group_quotient_cent_prime [in mathcomp.solvable.pgroup]
p'natE [in mathcomp.ssreflect.prime]
p'natEpi [in mathcomp.ssreflect.prime]
p'nat_coprime [in mathcomp.ssreflect.prime]
p'_elt_constt [in mathcomp.solvable.pgroup]
p1ElemE [in mathcomp.solvable.abelian]
p2Elem_dprodP [in mathcomp.solvable.abelian]
p2group_abelian [in mathcomp.solvable.sylow]
p3group_extraspecial [in mathcomp.solvable.maximal]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (100113 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1864 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49278 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1631 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6978 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (94 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14781 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (131 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2030 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2189 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1149 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19126 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (565 entries) |