B (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 |
B (Abbreviations)
band [abbrev, in mathcomp.algebra.mxpoly]BaseFinGroup [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.arg_sort [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.clone [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.copy [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.on [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.sort [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup_isGroup [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup_isGroup.Build [abbrev, in mathcomp.finite_group.fingroup]
baseFinGroupType [abbrev, in mathcomp.finite_group.fingroup]
BaseGroup [abbrev, in mathcomp.boot.monoid]
BaseGroup.clone [abbrev, in mathcomp.boot.monoid]
BaseGroup.copy [abbrev, in mathcomp.boot.monoid]
BaseGroup.Exports.baseGroupType [abbrev, in mathcomp.boot.monoid]
BaseGroup.on [abbrev, in mathcomp.boot.monoid]
BaseGroup.on_ [abbrev, in mathcomp.boot.monoid]
BaseUMagma [abbrev, in mathcomp.boot.monoid]
BaseUMagma.clone [abbrev, in mathcomp.boot.monoid]
BaseUMagma.copy [abbrev, in mathcomp.boot.monoid]
BaseUMagma.Exports.baseUMagmaType [abbrev, in mathcomp.boot.monoid]
BaseUMagma.on [abbrev, in mathcomp.boot.monoid]
BaseUMagma.on_ [abbrev, in mathcomp.boot.monoid]
BaseUMagma_isUMagma [abbrev, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.axioms [abbrev, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.Build [abbrev, in mathcomp.boot.monoid]
BIG_F [abbrev, in mathcomp.boot.bigop]
big_ord1 [abbrev, in mathcomp.algebra.zmodp]
big_ord1_cond [abbrev, in mathcomp.algebra.zmodp]
BIG_P [abbrev, in mathcomp.boot.bigop]
bigmax_sup_seq [abbrev, in mathcomp.boot.bigop]
bigop [abbrev, in mathcomp.boot.bigop]
Bilinear [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.clone [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.copy [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.Exports.bilinear [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.on [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.on_ [abbrev, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear [abbrev, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.axioms [abbrev, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.Build [abbrev, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.bilinear [abbrev, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.biscalar [abbrev, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.mapUUV [abbrev, in mathcomp.algebra.sesquilinear]
BLeft [abbrev, in mathcomp.algebra.interval]
BRight [abbrev, in mathcomp.algebra.interval]
bsCA [abbrev, in mathcomp.boot.seq]
Builders_1.conj [abbrev, in mathcomp.field.algC]
Builders_1.conj_nt [abbrev, in mathcomp.field.algC]
Builders_1.conjK [abbrev, in mathcomp.field.algC]
Builders_1.dim [abbrev, in mathcomp.algebra.vector]
Builders_1.inv [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.mul [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.mul [abbrev, in mathcomp.boot.monoid]
Builders_1.mul1g [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.mulgA [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_1.mulVg [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.one [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.solve_monicpoly [abbrev, in mathcomp.field.closed_field]
Builders_1.vector_subdef [abbrev, in mathcomp.algebra.vector]
Builders_10.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_10.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_10.one [abbrev, in mathcomp.boot.monoid]
Builders_13.normal_field_splitting_axiom [abbrev, in mathcomp.field.galois]
Builders_17.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_17.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_17.one [abbrev, in mathcomp.boot.monoid]
Builders_23.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_28.mul [abbrev, in mathcomp.boot.monoid]
Builders_28.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_28.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_28.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_28.one [abbrev, in mathcomp.boot.monoid]
Builders_41.inv [abbrev, in mathcomp.boot.monoid]
Builders_41.invgK [abbrev, in mathcomp.boot.monoid]
Builders_41.invgM [abbrev, in mathcomp.boot.monoid]
Builders_41.mul [abbrev, in mathcomp.boot.monoid]
Builders_41.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_41.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_41.one [abbrev, in mathcomp.boot.monoid]
Builders_53.mulgV [abbrev, in mathcomp.boot.monoid]
Builders_53.mulVg [abbrev, in mathcomp.boot.monoid]
Builders_60.inv [abbrev, in mathcomp.boot.monoid]
Builders_60.mul [abbrev, in mathcomp.boot.monoid]
Builders_60.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_60.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_60.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_60.mulgV [abbrev, in mathcomp.boot.monoid]
Builders_60.mulVg [abbrev, in mathcomp.boot.monoid]
Builders_60.one [abbrev, in mathcomp.boot.monoid]
Builders_77.pickle [abbrev, in mathcomp.boot.choice]
Builders_77.pickleK [abbrev, in mathcomp.boot.choice]
Builders_77.unpickle [abbrev, in mathcomp.boot.choice]
Builders_82.gmulfF [abbrev, in mathcomp.boot.monoid]