I (Abbreviations)
| 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 (Abbreviations)
I [abbrev, in mathcomp.algebra.ring_quotient]I [abbrev, in mathcomp.algebra.ring_quotient]
iC [abbrev, in mathcomp.group_representation.character]
Idealr [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.clone [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.copy [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.Exports.idealr [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.on [abbrev, in mathcomp.algebra.ring_quotient]
Idealr.on_ [abbrev, in mathcomp.algebra.ring_quotient]
idempotent [abbrev, in mathcomp.boot.ssrfun]
iG [abbrev, in mathcomp.group_representation.mxrepresentation]
Iirr [abbrev, in mathcomp.group_representation.character]
image [abbrev, in mathcomp.boot.fintype]
imset [abbrev, in mathcomp.boot.finset]
imset2 [abbrev, in mathcomp.boot.finset]
in_sub_seq [abbrev, in mathcomp.boot.fintype]
inA [abbrev, in mathcomp.solvable.hall]
infE [abbrev, in mathcomp.solvable.burnside_app]
infH [abbrev, in mathcomp.finite_group.action]
inG [abbrev, in mathcomp.solvable.hall]
inH [abbrev, in mathcomp.finite_group.action]
inlined_new_rect [abbrev, in mathcomp.boot.eqtype]
inlined_sub_rect [abbrev, in mathcomp.boot.eqtype]
intCK [abbrev, in mathcomp.field.cyclotomic]
Internals.add_term [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.and_cnf [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.CFactor [abbrev, in mathcomp.algebra.ring_tactic]
Internals.check_inconsistent [abbrev, 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_formulasT [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.clause [abbrev, 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.cnf [abbrev, 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_negate [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_normalise [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_of_GFormula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_of_list [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_tt [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cnf_tt [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.cond_norm [abbrev, in mathcomp.algebra.field_tactic]
Internals.cond_norm [abbrev, in mathcomp.algebra.field_tactic]
Internals.deduce [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.default_isIn [abbrev, in mathcomp.algebra.field_tactic]
Internals.env_nth [abbrev, in mathcomp.algebra.ring_tactic]
Internals.env_nth [abbrev, in mathcomp.algebra.ring_tactic]
Internals.env_nth [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_or_cnf [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.eval_Psatz [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.expN [abbrev, in mathcomp.algebra.ring_tactic]
Internals.F_of_N [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Fcons0 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons00 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons1 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons1 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons2 [abbrev, in mathcomp.algebra.field_tactic]
Internals.Fcons2 [abbrev, 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.Feval [abbrev, in mathcomp.algebra.arithmetic_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.Fnorm [abbrev, in mathcomp.algebra.field_tactic]
Internals.is_tauto [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.isIn [abbrev, in mathcomp.algebra.field_tactic]
Internals.Meval [abbrev, in mathcomp.algebra.ring_tactic]
Internals.MFactor [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mk_monpol_list [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mk_monpol_list [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkPX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkPX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.mkX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Mnorm [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Mon_of_Pol [abbrev, in mathcomp.algebra.ring_tactic]
Internals.negate [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.negate_aux [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.NFeval [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.nformula_plus_nformula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.nformula_times_nformula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.norm_subst [abbrev, in mathcomp.algebra.ring_tactic]
Internals.norm_subst [abbrev, 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.NPEadd [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEmul [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEopp [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEpow [abbrev, in mathcomp.algebra.field_tactic]
Internals.NPEsub [abbrev, in mathcomp.algebra.field_tactic]
Internals.or_clause [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.or_clause_cnf [abbrev, 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.P0 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P0 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P0 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.P1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Padd [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Padd [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PaddX [abbrev, 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.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_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.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.PEsimp [abbrev, in mathcomp.algebra.field_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.PExpr_eq [abbrev, in mathcomp.algebra.field_tactic]
Internals.pexpr_times_nformula [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.Pmul [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Pmul [abbrev, 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.PmulI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PmulI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PNSubst [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PNSubst1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PNSubstL [abbrev, 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.POneSubst [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Popp [abbrev, 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_pos [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Ppow_pos [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Psquare [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.Psub [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PsubC [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PsubI [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PSubstL [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PSubstL1 [abbrev, in mathcomp.algebra.ring_tactic]
Internals.PsubX [abbrev, in mathcomp.algebra.ring_tactic]
Internals.R_of_N [abbrev, in mathcomp.algebra.ring_tactic]
Internals.R_of_Z [abbrev, 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.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.Rnorm [abbrev, in mathcomp.algebra.ring_tactic]
Internals.Rnorm_expr [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.split [abbrev, in mathcomp.algebra.field_tactic]
Internals.split_aux [abbrev, in mathcomp.algebra.field_tactic]
Internals.sub [abbrev, in mathcomp.algebra.field_tactic]
Internals.sub [abbrev, in mathcomp.algebra.field_tactic]
Internals.tauto_checker [abbrev, in mathcomp.algebra.arithmetic_tactic]
Internals.unsat [abbrev, in mathcomp.algebra.arithmetic_tactic]
intOrdered.normz [abbrev, in mathcomp.algebra.ssrint]
intr [abbrev, in mathcomp.algebra.ssrint]
intrp [abbrev, in mathcomp.field.cyclotomic]
intrp [abbrev, in mathcomp.field.algnum]
intrp [abbrev, in mathcomp.field.algC]
InvClosed [abbrev, in mathcomp.boot.monoid]
InvClosed.clone [abbrev, in mathcomp.boot.monoid]
InvClosed.copy [abbrev, in mathcomp.boot.monoid]
InvClosed.Exports.invgClosed [abbrev, in mathcomp.boot.monoid]
InvClosed.on [abbrev, in mathcomp.boot.monoid]
InvClosed.on_ [abbrev, in mathcomp.boot.monoid]
invg [abbrev, in mathcomp.finite_group.fingroup]
invg1 [abbrev, in mathcomp.finite_group.fingroup]
invg_comm [abbrev, in mathcomp.finite_group.fingroup]
invg_inj [abbrev, in mathcomp.finite_group.fingroup]
invgK [abbrev, in mathcomp.finite_group.fingroup]
invMg [abbrev, in mathcomp.finite_group.fingroup]
InvolutiveRMorphism [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.clone [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.copy [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.Exports.involutive_rmorphism [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.on [abbrev, in mathcomp.algebra.sesquilinear]
InvolutiveRMorphism.on_ [abbrev, in mathcomp.algebra.sesquilinear]
inZp [abbrev, in mathcomp.algebra.zmodp]
iotaPz [abbrev, in mathcomp.field.fieldext]
irr [abbrev, in mathcomp.group_representation.character]
irr_comp'_op0 [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_comp_envelop [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_comp_id [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_comp_rsim [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_mx_mult [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_mx_sum [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_repr'_op0 [abbrev, in mathcomp.group_representation.mxrepresentation]
irr_reprK [abbrev, in mathcomp.group_representation.mxrepresentation]
is_orthogonal [abbrev, in mathcomp.algebra.sesquilinear]
is_symplectic [abbrev, in mathcomp.algebra.sesquilinear]
isBilinear [abbrev, in mathcomp.algebra.sesquilinear]
isBilinear.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isBilinear.Build [abbrev, in mathcomp.algebra.sesquilinear]
isComplex [abbrev, in mathcomp.field.algC]
isComplex.axioms [abbrev, in mathcomp.field.algC]
isComplex.Build [abbrev, in mathcomp.field.algC]
isCountable [abbrev, in mathcomp.boot.choice]
isCountable.axioms [abbrev, in mathcomp.boot.choice]
isCountable.Build [abbrev, in mathcomp.boot.choice]
isDotProduct [abbrev, in mathcomp.algebra.sesquilinear]
isDotProduct.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isDotProduct.Build [abbrev, in mathcomp.algebra.sesquilinear]
isEqQuotient [abbrev, in mathcomp.boot.generic_quotient]
isEqQuotient.axioms [abbrev, in mathcomp.boot.generic_quotient]
isEqQuotient.Build [abbrev, in mathcomp.boot.generic_quotient]
isFinite [abbrev, in mathcomp.boot.fintype]
isFinite.axioms [abbrev, in mathcomp.boot.fintype]
isFinite.Build [abbrev, in mathcomp.boot.fintype]
isGroup [abbrev, in mathcomp.boot.monoid]
isGroup.axioms [abbrev, in mathcomp.boot.monoid]
isGroup.Build [abbrev, in mathcomp.boot.monoid]
isGroupMorphism [abbrev, in mathcomp.boot.monoid]
isGroupMorphism.axioms [abbrev, in mathcomp.boot.monoid]
isGroupMorphism.Build [abbrev, in mathcomp.boot.monoid]
isHermitianSesquilinear [abbrev, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isHermitianSesquilinear.Build [abbrev, in mathcomp.algebra.sesquilinear]
isIdealr [abbrev, in mathcomp.algebra.ring_quotient]
isIdealr.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isIdealr.Build [abbrev, in mathcomp.algebra.ring_quotient]
isInvClosed [abbrev, in mathcomp.boot.monoid]
isInvClosed.axioms [abbrev, in mathcomp.boot.monoid]
isInvClosed.Build [abbrev, in mathcomp.boot.monoid]
isInvolutive [abbrev, in mathcomp.algebra.sesquilinear]
isInvolutive.axioms [abbrev, in mathcomp.algebra.sesquilinear]
isInvolutive.Build [abbrev, in mathcomp.algebra.sesquilinear]
isMonoid [abbrev, in mathcomp.boot.monoid]
isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
isMonoid.Build [abbrev, in mathcomp.boot.monoid]
isMul1Closed [abbrev, in mathcomp.boot.monoid]
isMul1Closed.axioms [abbrev, in mathcomp.boot.monoid]
isMul1Closed.Build [abbrev, in mathcomp.boot.monoid]
isMulBaseGroup [abbrev, in mathcomp.finite_group.fingroup]
isMulBaseGroup.Build [abbrev, in mathcomp.finite_group.fingroup]
isMulClosed [abbrev, in mathcomp.boot.monoid]
isMulClosed.axioms [abbrev, in mathcomp.boot.monoid]
isMulClosed.Build [abbrev, in mathcomp.boot.monoid]
isMulGroup [abbrev, in mathcomp.finite_group.fingroup]
isMulGroup.Build [abbrev, in mathcomp.finite_group.fingroup]
isMultiplicative [abbrev, in mathcomp.boot.monoid]
isMultiplicative.axioms [abbrev, in mathcomp.boot.monoid]
isMultiplicative.Build [abbrev, in mathcomp.boot.monoid]
isNzRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isNzRingQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
isob [abbrev, in mathcomp.solvable.center]
isPrimeIdealrClosed [abbrev, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isPrimeIdealrClosed.Build [abbrev, in mathcomp.algebra.ring_quotient]
isProperIdeal [abbrev, in mathcomp.algebra.ring_quotient]
isProperIdeal.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isProperIdeal.Build [abbrev, in mathcomp.algebra.ring_quotient]
isQuotient [abbrev, in mathcomp.boot.generic_quotient]
isQuotient.axioms [abbrev, in mathcomp.boot.generic_quotient]
isQuotient.Build [abbrev, in mathcomp.boot.generic_quotient]
isRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isRingQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
isSemigroup [abbrev, in mathcomp.boot.monoid]
isSemigroup.axioms [abbrev, in mathcomp.boot.monoid]
isSemigroup.Build [abbrev, in mathcomp.boot.monoid]
isStarMonoid [abbrev, in mathcomp.boot.monoid]
isStarMonoid.axioms [abbrev, in mathcomp.boot.monoid]
isStarMonoid.Build [abbrev, in mathcomp.boot.monoid]
isSub [abbrev, in mathcomp.boot.eqtype]
isSub.axioms [abbrev, in mathcomp.boot.eqtype]
isSub.Build [abbrev, in mathcomp.boot.eqtype]
isSubBaseUMagma [abbrev, in mathcomp.boot.monoid]
isSubBaseUMagma.axioms [abbrev, in mathcomp.boot.monoid]
isSubBaseUMagma.Build [abbrev, in mathcomp.boot.monoid]
isSubMagma [abbrev, in mathcomp.boot.monoid]
isSubMagma.axioms [abbrev, in mathcomp.boot.monoid]
isSubMagma.Build [abbrev, in mathcomp.boot.monoid]
isUMagmaMorphism [abbrev, in mathcomp.boot.monoid]
isUMagmaMorphism.axioms [abbrev, in mathcomp.boot.monoid]
isUMagmaMorphism.Build [abbrev, in mathcomp.boot.monoid]
isUnitRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isUnitRingQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
isZmodQuotient [abbrev, in mathcomp.algebra.ring_quotient]
isZmodQuotient.axioms [abbrev, in mathcomp.algebra.ring_quotient]
isZmodQuotient.Build [abbrev, in mathcomp.algebra.ring_quotient]
itv [abbrev, in mathcomp.algebra.interval_inference]
Itv.Exports.num [abbrev, in mathcomp.algebra.interval_inference]