G (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 |
G (Abbreviations)
G [abbrev, in mathcomp.group_representation.inertia]G [abbrev, in mathcomp.group_representation.classfun]
G [abbrev, in mathcomp.group_representation.classfun]
G [abbrev, in mathcomp.group_representation.classfun]
g [abbrev, in mathcomp.group_representation.character]
G' [abbrev, in mathcomp.solvable.hall]
G1 [abbrev, in mathcomp.group_representation.classfun]
G_ [abbrev, in mathcomp.solvable.center]
GaussE [abbrev, in mathcomp.algebra.mxalgebra]
Gaussian_elimination [abbrev, in mathcomp.algebra.mxalgebra]
generated [abbrev, in mathcomp.finite_group.fingroup]
genmx [abbrev, in mathcomp.algebra.mxalgebra]
gH [abbrev, in mathcomp.finite_group.gproduct]
gK [abbrev, in mathcomp.finite_group.gproduct]
gof [abbrev, in mathcomp.finite_group.morphism]
GRing.addKr_char2 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.addrClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.addrK_char2 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.addrr_char2 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Algebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Algebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Algebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Algebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.AllExports.addr_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.bin_lt_charf_0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Builders_1.add [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.add0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.addrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.addrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mul0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mulr0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mulr1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.mulrDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_1.zero [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_103.inv [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_103.invr0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_103.mulVf [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_12.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.mul0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.mulr0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.mulr1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.mulrDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_12.oner_neq0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_142.scale [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_142.scale1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_142.scalerA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_142.scalerDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_142.scalerDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_17.inv [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_17.invr_out [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_17.mulVx [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_17.unit [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_17.unitPl [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_19.add [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.add0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.addrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.addrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mul0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mulr0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mulr1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.mulrDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.oner_neq0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_19.zero [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_20.ok_proj [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Builders_20.proj [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Builders_20.wf_proj [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Builders_374.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_374.mul0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_374.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_374.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_374.mulrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_374.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_374.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.mul0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.mulrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_381.oner_neq0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.mulrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mulr1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mulrDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_406.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_406.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_406.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_406.mulrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_406.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_406.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_406.oner_neq0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_419.scalerAl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.add [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.add0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.addNr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.addrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.addrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.mulr1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.mulrDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.opp [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_45.zero [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_558.rpred1M [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.mulr1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.mulrDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_58.oner_neq0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.add [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.add0r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.addNr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.addrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.addrC [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.mul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.mul1r [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.mulr1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.mulrA [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.mulrDl [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.mulrDr [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.one [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.oner_neq0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.opp [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_65.zero [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_658.valZ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_96.fieldP [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.char0_natf_div [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.char_lalg [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.charf'_nat [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.charf0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.charf0P [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.charf_eq [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.charf_prime [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ClosedExports.divalg_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ClosedExports.divr_2closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ClosedExports.divr_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ClosedExports.divring_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ClosedExports.invr_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ClosedExports.linear_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.mulr_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.nmod_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.oppr_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.scaler_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.sdivr_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ClosedExports.semiring_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.smulr_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.subalg_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.submod_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.subring_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.subsemimod_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedExports.zmod_closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ClosedField [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.Exports.closedFieldType [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ComAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComAlgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComNzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.comNzAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.comNzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing_hasMulInverse [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_hasMulInverse.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_hasMulInverse.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_isField [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_isField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_isField.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.comNzSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.Exports.comNzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.comPzAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.Exports.comPzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.Exports.comPzSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.Exports.comPzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComRing.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComRing_hasMulInverse [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComRing_hasMulInverse.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComRing_isField [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComRing_isField.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiAlgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComSemiRing.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.ComUnitAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.comUnitAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.Exports.comUnitRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isField [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isField.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isIntegral [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isIntegral.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isIntegral.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DecField_isAlgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecField_isAlgClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecField_isAlgClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.Exports.decFieldType [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DivalgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.divalgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.Exports.divClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.divringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.dvdn_charf [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.exprDn_char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.exprNn_char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.f'E [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.False [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field.Exports.fieldType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field_isDecField [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_isDecField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_isDecField.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_QE_isDecField [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_QE_isDecField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_QE_isDecField.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.fmorph_char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_aut [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_aut0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_aut1 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_aut_nat [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_autB_comm [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_autD_comm [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_autE [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_autM_comm [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_autMn [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_autN [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Frobenius_autX [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.has_char0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.has_pchar0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.IntegralDomain [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.Exports.idomainType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivalgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivalgClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivalgClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivringClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivringClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isInvClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isInvClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isInvClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isLinear [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isLinear.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isLinear.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMonoidMorphism [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMonoidMorphism.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMonoidMorphism.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul1Closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul1Closed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul1Closed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul2Closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul2Closed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul2Closed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMulClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMulClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMulClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMultiplicative [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isMultiplicative.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isMultiplicative.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isScalable [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScalable.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScalable.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScaleClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScaleClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScaleClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSdivClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isSdivClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isSdivClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isSemilinear [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemilinear.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemilinear.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isSemiringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemiringClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemiringClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSmulClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSmulClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSmulClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubalgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubalgClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubalgClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLmodule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLmodule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLmodule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLSemiModule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLSemiModule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLSemiModule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubmodClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubmodClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubmodClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubPzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubPzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubringClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubringClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiAlgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiAlgClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiAlgClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiModClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiModClosed.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiModClosed.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isSubSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra_isAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra_isAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra_isComAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lalgebra_isComAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Linear [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Linear.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Linear.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Linear.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Linear.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.linear [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.Linear.mapUV [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.scalable [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.scalar [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.semilinear [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.semiscalar [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.Exports.lmodType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule_isLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Lmodule_isLalgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.LRMorphism [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.LSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.LSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.LSemiAlgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.LSemiAlgebra_isComSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isComSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isComSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.Exports.lSemiModType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isComSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isComSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isComSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLmodule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLmodule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLmodule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MathCompCompatClosedField.ClosedField.axiom [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatClosedField.ClosedField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatClosedField.ClosedField.class_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatClosedField.ClosedField.mcpack [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatClosedField.ClosedField.Mixin [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatClosedField.ClosedField.mixin_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatDecidableField.DecidableField.axiom [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatDecidableField.DecidableField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatDecidableField.DecidableField.class_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatDecidableField.DecidableField.mcpack [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatDecidableField.DecidableField.Mixin [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatDecidableField.DecidableField.mixin_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatField.Field.axiom [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatField.Field.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatField.Field.class_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatField.Field.mcpack [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatField.Field.Mixin [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatField.Field.mixin_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatIntegralDomain.IntegralDomain.axiom [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatIntegralDomain.IntegralDomain.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatIntegralDomain.IntegralDomain.class_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatIntegralDomain.IntegralDomain.mcpack [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatIntegralDomain.IntegralDomain.Mixin [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatIntegralDomain.IntegralDomain.mixin_of [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Mul2Closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.Exports.mulr2Closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.Exports.mulrClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrn_char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.natf0_char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.natf_neq0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.natr_mod_char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Nmodule_isComNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComNzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComNzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComPzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComPzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Nmodule_isComSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Nmodule_isLSemiModule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isLSemiModule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isLSemiModule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isNzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isNzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isPzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isPzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Nmodule_isSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.NzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.nzAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.nzLalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.Exports.nzLSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.Exports.nzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing_hasMulInverse [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.NzRing_hasMulInverse.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.NzRing_hasMulInverse.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.NzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.Exports.nzSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.Exports.nzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.oppr_char2 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.opprClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_aut_is_multiplicative [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.PzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.Exports.pzAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.pzLalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.Exports.pzLSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.Exports.pzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing_hasCommutativeMul [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.PzRing_hasCommutativeMul.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.PzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.Exports.pzSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.Exports.pzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing_hasCommutativeMul [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.PzSemiRing_hasCommutativeMul.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.PzSemiRing_isNonZero [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing_isNonZero.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing_isNonZero.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Ring [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Ring.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Ring.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Ring.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Ring_hasCommutativeMul [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Ring_hasCommutativeMul.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Ring_hasMulInverse [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Ring_hasMulInverse.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.rmorph_char [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.RMorphism [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.RMorphism.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.RMorphism.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.RMorphism.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.RMorphism.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isLaw [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isLaw.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isLaw.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isPreLaw [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isPreLaw.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isPreLaw.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isSemiLaw [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isSemiLaw.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isSemiLaw.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SdivClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.Exports.sdivClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SemiAlgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SemiRing.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Semiring2Closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.Exports.semiring2Closed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiRing_hasCommutativeMul [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiRing_hasCommutativeMul.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiRing_hasCommutativeMul.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.Exports.semiringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sign [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.Exports.smulClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.Exports.subalgClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubAlgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubComNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubComRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubComSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubComSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubComUnitRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubComUnitRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubComUnitRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubIntegralDomain [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubIntegralDomain.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubIntegralDomain.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubLmodule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLmodule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLmodule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLSemiModule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLSemiModule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLSemiModule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLalgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLalgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLalgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLalgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubChoice_isSubUnitRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubUnitRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubUnitRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.subComNzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.subComNzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.subComPzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.subComPzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComRing.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComSemiRing.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubComUnitRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.subComUnitRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing_isSubIntegralDomain [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing_isSubIntegralDomain.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing_isSubIntegralDomain.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.subFieldType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.subIdomainType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain_isSubField [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain_isSubField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain_isSubField.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLalgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLalgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLalgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLmodule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.subLmodType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLSemiAlgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubLSemiAlgebra_isSubSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiAlgebra_isSubSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiAlgebra_isSubSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.Exports.subLSemiModType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.Exports.submodClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubLSemiModule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubLSemiModule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubLSemiModule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubNzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubNzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubPzSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubPzSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubNmodule_isSubSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubNzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.subNzAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.subNzLalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.subNzLSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.subNzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing_isSubUnitRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubNzRing_isSubUnitRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubNzRing_isSubUnitRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubNzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.subNzSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.subNzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.subPzAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.subPzLalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.subPzLSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.subPzRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing_isSubComPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubPzRing_isSubComPzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubPzRing_isSubComPzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubPzSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.subPzSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.Exports.subPzSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing_isNonZero [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing_isNonZero.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing_isNonZero.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subr_char2 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubRing.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubRing_SubLmodule_isSubLalgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubRing_SubLmodule_isSubLalgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubRing_SubLmodule_isSubLalgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.subringClosed [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiAlgebra.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiRing.sort [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubSemiRing_isSubComSemiRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_isSubComSemiRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_isSubComSemiRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_SubLSemiModule_isSubLSemiAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_SubLSemiModule_isSubLSemiAlgebra.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_SubLSemiModule_isSubLSemiAlgebra.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubUnitRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.subUnitRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubZmodule_isSubNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubZmodule_isSubNzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubZmodule_isSubPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubZmodule_isSubPzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubZmodule_isSubRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubZmodule_isSubRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.in_alg [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.null_fun [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.True [abbrev, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.UnitAlgebra [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.unitAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.clone [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.copy [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.Exports.unitRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.on [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.on_ [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing_isField [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing_isField.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing_isField.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.val [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.val [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComNzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComNzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComPzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComPzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Zmodule_isComRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Zmodule_isLmodule [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isLmodule.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isLmodule.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isNzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isNzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isNzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isPzRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isPzRing.axioms [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isPzRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isRing [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Zmodule_isRing.Build [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
gring_irr_mode [abbrev, in mathcomp.group_representation.integral_char]
Group [abbrev, in mathcomp.boot.monoid]
Group.clone [abbrev, in mathcomp.boot.monoid]
Group.copy [abbrev, in mathcomp.boot.monoid]
Group.Exports.groupType [abbrev, in mathcomp.boot.monoid]
Group.on [abbrev, in mathcomp.boot.monoid]
Group.on_ [abbrev, in mathcomp.boot.monoid]
GroupClosed [abbrev, in mathcomp.boot.monoid]
GroupClosed.clone [abbrev, in mathcomp.boot.monoid]
GroupClosed.copy [abbrev, in mathcomp.boot.monoid]
GroupClosed.Exports.groupClosed [abbrev, in mathcomp.boot.monoid]
GroupClosed.on [abbrev, in mathcomp.boot.monoid]
GroupClosed.on_ [abbrev, in mathcomp.boot.monoid]
groupT [abbrev, in mathcomp.solvable.gseries]
groupT [abbrev, in mathcomp.finite_group.fingroup]
gsort [abbrev, in mathcomp.finite_group.fingroup]
gT [abbrev, in mathcomp.finite_group.action]
gTg [abbrev, in mathcomp.solvable.jordanholder]
gTn [abbrev, in mathcomp.finite_group.gproduct]
gtype [abbrev, in mathcomp.solvable.extraspecial]