G (Definitions)
| 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 (Definitions)
gacent [def, in mathcomp.finite_group.action]gacent_group [def, in mathcomp.finite_group.action]
gact_range [def, in mathcomp.finite_group.action]
gal [def, in mathcomp.field.galois]
gal_inv [def, in mathcomp.field.galois]
gal_morphism [def, in mathcomp.field.galois]
gal_mul [def, in mathcomp.field.galois]
gal_one [def, in mathcomp.field.galois]
gal_repr [def, in mathcomp.field.galois]
gal_sgval [def, in mathcomp.field.galois]
galNorm [def, in mathcomp.field.galois]
galois [def, in mathcomp.field.galois]
galoisG [def, in mathcomp.field.galois]
galoisG_group [def, in mathcomp.field.galois]
galTrace [def, in mathcomp.field.galois]
galTrace_is_additive [def, in mathcomp.field.galois]
Gaussian_elimination.body [def, in mathcomp.algebra.mxalgebra]
Gaussian_elimination.unlock [def, in mathcomp.algebra.mxalgebra]
Gaussian_elimination_ [def, in mathcomp.algebra.mxalgebra]
Gaussian_elimination_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
Gaussian_elimination_unlockable [def, in mathcomp.algebra.mxalgebra]
gcard [def, in mathcomp.group_representation.mxrepresentation]
gcdn [def, in mathcomp.boot.div]
gcdz [def, in mathcomp.algebra.intdiv]
gcore [def, in mathcomp.finite_group.fingroup]
gcore_group [def, in mathcomp.finite_group.fingroup]
geigenspace [def, in mathcomp.algebra.mxpoly]
gen_rank [def, in mathcomp.solvable.abelian]
generated.body [def, in mathcomp.finite_group.fingroup]
generated.unlock [def, in mathcomp.finite_group.fingroup]
generated_group [def, in mathcomp.finite_group.fingroup]
generated_unlock_subterm [def, in mathcomp.finite_group.fingroup]
generated_unlockable [def, in mathcomp.finite_group.fingroup]
generator [def, in mathcomp.solvable.cyclic]
genmx.body [def, in mathcomp.algebra.mxalgebra]
genmx.unlock [def, in mathcomp.algebra.mxalgebra]
genmx_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
genmx_unlockable [def, in mathcomp.algebra.mxalgebra]
genmx_witness [def, in mathcomp.algebra.mxalgebra]
GenTree.decode [def, in mathcomp.boot.choice]
GenTree.decode_step [def, in mathcomp.boot.choice]
GenTree.encode [def, in mathcomp.boot.choice]
GenTree.tree_ind [def, in mathcomp.boot.choice]
GenTree.tree_rec [def, in mathcomp.boot.choice]
GenTree.tree_rect [def, in mathcomp.boot.choice]
geq [def, in mathcomp.boot.ssrnat]
gFcomp_gFun [def, in mathcomp.solvable.gfunctor]
gFcomp_igFun [def, in mathcomp.solvable.gfunctor]
gFcomp_mgFun [def, in mathcomp.solvable.gfunctor]
gFgroup [def, in mathcomp.solvable.gfunctor]
gFmod_gFun [def, in mathcomp.solvable.gfunctor]
gFmod_group [def, in mathcomp.solvable.gfunctor]
gFmod_igFun [def, in mathcomp.solvable.gfunctor]
gFmod_pgFun [def, in mathcomp.solvable.gfunctor]
gFunc_id [def, in mathcomp.solvable.gfunctor]
GFunctor.clone [def, in mathcomp.solvable.gfunctor]
GFunctor.clone_iso [def, in mathcomp.solvable.gfunctor]
GFunctor.clone_mono [def, in mathcomp.solvable.gfunctor]
GFunctor.clone_pmap [def, in mathcomp.solvable.gfunctor]
GFunctor.closed [def, in mathcomp.solvable.gfunctor]
GFunctor.comp [def, in mathcomp.solvable.gfunctor]
GFunctor.continuous [def, in mathcomp.solvable.gfunctor]
GFunctor.group_valued [def, in mathcomp.solvable.gfunctor]
GFunctor.hereditary [def, in mathcomp.solvable.gfunctor]
GFunctor.iso_continuous [def, in mathcomp.solvable.gfunctor]
GFunctor.modulo [def, in mathcomp.solvable.gfunctor]
GFunctor.monotonic [def, in mathcomp.solvable.gfunctor]
GFunctor.object_map [def, in mathcomp.solvable.gfunctor]
GFunctor.pack_iso [def, in mathcomp.solvable.gfunctor]
GFunctor.pcontinuous [def, in mathcomp.solvable.gfunctor]
GLgroup [def, in mathcomp.algebra.matrix]
GLgroup_group [def, in mathcomp.algebra.matrix]
GLrepr [def, in mathcomp.group_representation.mxabelem]
GLtype [def, in mathcomp.algebra.matrix]
GLval [def, in mathcomp.algebra.matrix]
gmulf1 [def, in mathcomp.boot.monoid]
gmulfM [def, in mathcomp.boot.monoid]
gnorm [def, in mathcomp.boot.monoid]
gpred1 [def, in mathcomp.boot.monoid]
gpredM [def, in mathcomp.boot.monoid]
gpredVr [def, in mathcomp.boot.monoid]
grel [def, in mathcomp.boot.fingraph]
grepr0 [def, in mathcomp.group_representation.character]
GRing.additive_linear [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.additive_semilinear [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.addr_closed [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.and_dnf [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Builders_147.opp [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_20.qe_is_def_field [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Builders_374.mulr1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_374.mulrDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.mulr1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_399.mulrDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.can2_rmorphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.closed_field_axiom [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ClosedField.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_Algebra_BaseZmodule_and_GRing_ComNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_ComNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_ComPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_ComPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_Lmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_LSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_ComPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_ComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_Lmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiRing_and_GRing_ComPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiRing_and_GRing_Lmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiRing_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiRing_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiRing_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComNzSemiRing_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzAlgebra_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzAlgebra_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzAlgebra_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzAlgebra_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzAlgebra_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzAlgebra_and_GRing_NzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzRing_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzRing_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzRing_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzRing_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzSemiRing_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.Exports.join_GRing_ComNzAlgebra_between_GRing_ComPzSemiRing_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_Algebra_BaseZmodule_and_GRing_ComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_GRing_ComNzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_GRing_ComNzSemiRing_and_GRing_ComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_GRing_ComNzSemiRing_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_GRing_ComNzSemiRing_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_GRing_ComPzRing_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_GRing_ComPzRing_and_GRing_NzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.Exports.join_GRing_ComNzRing_between_GRing_ComPzSemiRing_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzRing_hasMulInverse.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_hasMulInverse.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_isField.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzRing_isField.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComNzSemiRing_and_GRing_ComPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComNzSemiRing_and_GRing_LSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComNzSemiRing_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComNzSemiRing_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComNzSemiRing_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComNzSemiRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_NzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComPzSemiRing_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.Exports.join_GRing_ComNzSemiAlgebra_between_GRing_ComPzSemiRing_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.Exports.join_GRing_ComNzSemiRing_between_GRing_ComPzSemiRing_and_GRing_NzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComNzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_Algebra_BaseZmodule_and_GRing_ComPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzRing_and_GRing_ComPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzRing_and_GRing_Lmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzRing_and_GRing_LSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzRing_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzRing_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzRing_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_Lmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiRing_and_GRing_Lmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiRing_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.Exports.join_GRing_ComPzAlgebra_between_GRing_ComPzSemiRing_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.Exports.join_GRing_ComPzRing_between_Algebra_BaseZmodule_and_GRing_ComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.Exports.join_GRing_ComPzRing_between_GRing_ComPzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.Exports.join_GRing_ComPzRing_between_GRing_ComPzSemiRing_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.Exports.join_GRing_ComPzSemiAlgebra_between_GRing_ComPzSemiRing_and_GRing_LSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.Exports.join_GRing_ComPzSemiAlgebra_between_GRing_ComPzSemiRing_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.Exports.join_GRing_ComPzSemiAlgebra_between_GRing_ComPzSemiRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComPzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzAlgebra_and_GRing_ComUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzAlgebra_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzRing_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_ComUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzSemiAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComNzSemiRing_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzAlgebra_and_GRing_ComUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzAlgebra_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzRing_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_ComUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzSemiAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComPzSemiRing_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_Lmodule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_LSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_NzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_NzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.Exports.join_GRing_ComUnitAlgebra_between_GRing_ComUnitRing_and_GRing_UnitAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.Exports.join_GRing_ComUnitRing_between_GRing_ComNzRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.Exports.join_GRing_ComUnitRing_between_GRing_ComNzSemiRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.Exports.join_GRing_ComUnitRing_between_GRing_ComPzRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.Exports.join_GRing_ComUnitRing_between_GRing_ComPzSemiRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isField.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isField.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isIntegral.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isIntegral.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.ComUnitRing_isIntegral.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.converse [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.DecField_isAlgClosed.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecField_isAlgClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecField_isAlgClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.decidable_field_axiom [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.DecidableField.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.divalg_closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_Algebra_OppClosed_and_GRing_SubalgClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_Algebra_OppClosed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_DivClosed_and_GRing_SubalgClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_DivClosed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_DivringClosed_and_GRing_SubalgClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_DivringClosed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SdivClosed_and_GRing_SubalgClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SdivClosed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SmulClosed_and_GRing_SubalgClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SmulClosed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SubalgClosed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SubalgClosed_and_GRing_SubringClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SubmodClosed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.Exports.join_GRing_DivalgClosed_between_GRing_SubmodClosed_and_GRing_SubringClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivalgClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divfK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divr_2closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divr_closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divring_closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_Algebra_AddClosed_and_GRing_DivClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_Algebra_AddClosed_and_GRing_SdivClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_DivClosed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_DivClosed_and_GRing_Semiring2Closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_DivClosed_and_GRing_SemiringClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_DivClosed_and_GRing_SubringClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_SdivClosed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_SdivClosed_and_GRing_Semiring2Closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_SdivClosed_and_GRing_SemiringClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.Exports.join_GRing_DivringClosed_between_GRing_SdivClosed_and_GRing_SubringClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.DivringClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divrK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.dnf_rterm [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.dnf_to_form [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eq0_rform [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eval [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.exp [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Field.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.field_axiom [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Field_isDecField.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_isDecField.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_isDecField.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_QE_isDecField.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Field_QE_isDecField.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.fieldP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fsubst [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.holds [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.If [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.in_alg [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.integral_domain_axiom [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.IntegralDomain.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.inv [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivalgClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivalgClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivringClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isDivringClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isInvClosed.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isInvClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isInvClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isLinear.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isLinear.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMonoidMorphism.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMonoidMorphism.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMonoidMorphism.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul1Closed.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul1Closed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul1Closed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul2Closed.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul2Closed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMul2Closed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMulClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMulClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isMultiplicative.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isMultiplicative.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.isNzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isNzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isPzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScalable.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScalable.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScalable.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScaleClosed.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScaleClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isScaleClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSdivClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isSdivClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.isSemilinear.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemilinear.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemiringClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSemiringClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSmulClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSmulClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubalgClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubalgClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLmodule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLmodule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLSemiModule.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLSemiModule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubLSemiModule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubmodClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubmodClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubPzSemiRing.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubPzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubPzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubringClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubringClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiAlgClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiAlgClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiModClosed.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.isSubSemiModClosed.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Linear.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Linear.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Linear.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linear_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linear_for [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.Linear.map_at [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.Linear.map_class [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.Linear.unify_map_at [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LinearExports.Linear.wrap [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.Exports.join_GRing_Lmodule_between_Algebra_BaseZmodule_and_GRing_LSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.Exports.join_GRing_Lmodule_between_GRing_LSemiModule_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Lmodule.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lreg [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.Exports.join_GRing_LRMorphism_between_GRing_Linear_and_GRing_RMorphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LRMorphism.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isComSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isComSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isSemiAlgebra.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiAlgebra_isSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isComSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isComSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLmodule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLmodule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLSemiAlgebra.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.LSemiModule_isLSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MathCompCompatClosedField.ClosedField.phant_mcpack [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatDecidableField.DecidableField.phant_mcpack [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.MathCompCompatField.Field.phant_mcpack [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.MathCompCompatIntegralDomain.IntegralDomain.phant_mcpack [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.monoid_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mul [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mul0r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mul1r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Mul2Closed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mul_fun [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.MulClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulfV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mull_fun [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_2closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_fun [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrDl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.multiplicative [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.natr_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComNzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComNzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComPzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isComPzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isLSemiModule.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isLSemiModule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isLSemiModule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isNzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isNzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isPzSemiRing.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isPzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Nmodule_isPzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_Algebra_BaseZmodule_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_Lmodule_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzLalgebra_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzLalgebra_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzLalgebra_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzRing_and_GRing_NzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzRing_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.Exports.join_GRing_NzAlgebra_between_GRing_NzSemiRing_and_GRing_PzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_Algebra_BaseZmodule_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_Lmodule_and_GRing_NzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_Lmodule_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_Lmodule_and_GRing_NzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_LSemiModule_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_NzLSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_NzLSemiAlgebra_and_GRing_NzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_NzLSemiAlgebra_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_NzLSemiAlgebra_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_NzRing_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_NzRing_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.Exports.join_GRing_NzLalgebra_between_GRing_NzSemiRing_and_GRing_PzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLalgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.Exports.join_GRing_NzLSemiAlgebra_between_GRing_LSemiModule_and_GRing_NzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.Exports.join_GRing_NzLSemiAlgebra_between_GRing_NzSemiRing_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzLSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.Exports.join_GRing_NzRing_between_Algebra_BaseZmodule_and_GRing_NzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.Exports.join_GRing_NzRing_between_GRing_NzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.Exports.join_GRing_NzRing_between_GRing_NzSemiRing_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzRing_hasMulInverse.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.NzRing_hasMulInverse.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.NzRing_hasMulInverse.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.NzSemiAlgebra.Exports.join_GRing_NzSemiAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.Exports.join_GRing_NzSemiAlgebra_between_GRing_NzSemiRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.NzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.one [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.oner_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pchar [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_aut [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Pick [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.proj_sat [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.PzAlgebra.Exports.join_GRing_PzAlgebra_between_Algebra_BaseZmodule_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.Exports.join_GRing_PzAlgebra_between_GRing_Lmodule_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.Exports.join_GRing_PzAlgebra_between_GRing_PzLalgebra_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.Exports.join_GRing_PzAlgebra_between_GRing_PzRing_and_GRing_PzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.Exports.join_GRing_PzAlgebra_between_GRing_PzSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.join_GRing_PzLalgebra_between_Algebra_BaseZmodule_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.join_GRing_PzLalgebra_between_GRing_Lmodule_and_GRing_PzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.join_GRing_PzLalgebra_between_GRing_Lmodule_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.join_GRing_PzLalgebra_between_GRing_Lmodule_and_GRing_PzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.join_GRing_PzLalgebra_between_GRing_LSemiModule_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.join_GRing_PzLalgebra_between_GRing_PzLSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.Exports.join_GRing_PzLalgebra_between_GRing_PzLSemiAlgebra_and_GRing_PzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLalgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.Exports.join_GRing_PzLSemiAlgebra_between_GRing_LSemiModule_and_GRing_PzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzLSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.Exports.join_GRing_PzRing_between_Algebra_BaseZmodule_and_GRing_PzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.Exports.join_GRing_PzRing_between_GRing_PzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing_isNonZero.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing_isNonZero.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.PzSemiRing_isNonZero.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.qf_eval [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.qf_form [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.qf_to_dnf [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.quantifier_elim [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.regular [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.regular_field [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rformula [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.RMorphism.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.RMorphism.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.RMorphism.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphismMP [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.rpred1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpredM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpredVr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpredZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rreg [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rterm [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.same_env [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.sat [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.satP [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.scalable_for [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scale [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isLaw.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isLaw.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isLaw.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isPreLaw.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isPreLaw.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isPreLaw.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isSemiLaw.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isSemiLaw.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.isSemiLaw.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.law [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.Law.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.N1op [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.op0v [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.op1v [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.op_nmod_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.opA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.preLaw [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.PreLaw.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.semiLaw [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.SemiLaw.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scale0r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scale1r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scale_fun [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerAl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerAr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerDl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SdivClosed.Exports.join_GRing_SdivClosed_between_GRing_DivClosed_and_Algebra_OppClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.Exports.join_GRing_SdivClosed_between_GRing_DivClosed_and_GRing_SmulClosed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SdivClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.sdivr_closed [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.semilinear_for [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.Exports.join_GRing_Semiring2Closed_between_Algebra_AddClosed_and_GRing_Mul2Closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Semiring2Closed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.semiring_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiRing_hasCommutativeMul.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiRing_hasCommutativeMul.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiRing_hasCommutativeMul.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.Exports.join_GRing_SemiringClosed_between_Algebra_AddClosed_and_GRing_MulClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.Exports.join_GRing_SemiringClosed_between_GRing_MulClosed_and_GRing_Semiring2Closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SemiringClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.Exports.join_GRing_SmulClosed_between_GRing_Mul2Closed_and_Algebra_OppClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.Exports.join_GRing_SmulClosed_between_GRing_MulClosed_and_Algebra_OppClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SmulClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.smulr_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sol [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.solve_monicpoly [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.subalg_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.Exports.join_GRing_SubalgClosed_between_GRing_Mul2Closed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.Exports.join_GRing_SubalgClosed_between_GRing_MulClosed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.Exports.join_GRing_SubalgClosed_between_GRing_Semiring2Closed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.Exports.join_GRing_SubalgClosed_between_GRing_SemiringClosed_and_GRing_SubmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubalgClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComNzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComPzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubComUnitRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubComUnitRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubIntegralDomain.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubIntegralDomain.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubLmodule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLmodule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLSemiModule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubLSemiModule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLalgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLalgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzLSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubNzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLalgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLalgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzLSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubPzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubChoice_isSubUnitRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubChoice_isSubUnitRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_Algebra_BaseZmodule_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzSemiRing_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzSemiRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComNzSemiRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComPzRing_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComPzRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComPzRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_ComPzSemiRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_NzRing_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_NzRing_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_NzRing_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_NzSemiRing_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_PzRing_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComNzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComNzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComNzSemiRing_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComNzSemiRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComNzSemiRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComPzRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComPzRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.Exports.join_GRing_SubComNzRing_between_GRing_SubComPzSemiRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComNzSemiRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_ComPzSemiRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_NzSemiRing_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.Exports.join_GRing_SubComNzSemiRing_between_GRing_SubComPzSemiRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComNzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_Algebra_BaseZmodule_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_ComPzSemiRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_PzRing_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_SubComPzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_SubComPzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.Exports.join_GRing_SubComPzRing_between_GRing_SubComPzSemiRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.join_GRing_SubComPzSemiRing_between_GRing_ComPzSemiRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.join_GRing_SubComPzSemiRing_between_GRing_ComPzSemiRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.join_GRing_SubComPzSemiRing_between_GRing_ComPzSemiRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.join_GRing_SubComPzSemiRing_between_GRing_ComPzSemiRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.join_GRing_SubComPzSemiRing_between_GRing_ComPzSemiRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.join_GRing_SubComPzSemiRing_between_GRing_ComPzSemiRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.Exports.join_GRing_SubComPzSemiRing_between_GRing_ComPzSemiRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComPzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComNzRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComNzSemiRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComPzRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComPzSemiRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubComNzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_ComUnitRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComNzRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComNzRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComNzSemiRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComNzSemiRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComPzRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComPzRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComPzSemiRing_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.Exports.join_GRing_SubComUnitRing_between_GRing_SubComPzSemiRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing_isSubIntegralDomain.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubComUnitRing_isSubIntegralDomain.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubComNzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubComUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubIntegralDomain [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.Exports.join_GRing_SubField_between_GRing_Field_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubField.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubComNzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubComNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubComPzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubComPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubComUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.Exports.join_GRing_SubIntegralDomain_between_GRing_IntegralDomain_and_GRing_SubUnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain_isSubField.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubIntegralDomain_isSubField.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_Algebra_BaseZmodule_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_Lmodule_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_LSemiModule_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_SubLSemiModule_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.Exports.join_GRing_SubLmodule_between_GRing_SubLSemiModule_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLmodule.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiAlgebra_isSubSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiAlgebra_isSubSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.Exports.join_GRing_SubLSemiModule_between_GRing_LSemiModule_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.Exports.join_GRing_SubLSemiModule_between_GRing_LSemiModule_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.Exports.join_GRing_SubLSemiModule_between_GRing_LSemiModule_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.Exports.join_GRing_SubLSemiModule_between_GRing_LSemiModule_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.Exports.join_GRing_SubLSemiModule_between_GRing_LSemiModule_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.Exports.join_GRing_SubLSemiModule_between_GRing_LSemiModule_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubLSemiModule.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.submod_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubmodClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubLSemiModule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubLSemiModule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubNzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubNzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubPzSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNmodule_isSubPzSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_Algebra_BaseZmodule_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_Lmodule_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubNzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzAlgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzLalgebra_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzLalgebra_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzLalgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzRing_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzRing_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzRing_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubNzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_NzSemiRing_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzAlgebra_and_GRing_SubNzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzAlgebra_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzAlgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzAlgebra_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzAlgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzLalgebra_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzRing_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubNzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubLmodule_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzLalgebra_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzLalgebra_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzLalgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzLSemiAlgebra_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzRing_and_GRing_SubNzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzRing_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzRing_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzSemiAlgebra_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzSemiAlgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzSemiAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.Exports.join_GRing_SubNzAlgebra_between_GRing_SubNzSemiRing_and_GRing_SubPzAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_Algebra_BaseZmodule_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_Lmodule_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_Lmodule_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_Lmodule_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_LSemiModule_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLalgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzRing_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzRing_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzRing_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzRing_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzRing_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzSemiRing_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_NzSemiRing_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_PzLalgebra_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_PzLalgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_PzLalgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_PzLSemiAlgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_PzRing_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubLmodule_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubLmodule_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubLmodule_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubLSemiModule_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzLSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzLSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzLSemiAlgebra_and_GRing_SubNzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzLSemiAlgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzLSemiAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzRing_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzRing_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.Exports.join_GRing_SubNzLalgebra_between_GRing_SubNzSemiRing_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLalgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_LSemiModule_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzSemiRing_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_NzSemiRing_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_SubLSemiModule_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.Exports.join_GRing_SubNzLSemiAlgebra_between_GRing_SubNzSemiRing_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzLSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_Algebra_BaseZmodule_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_NzSemiRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_PzRing_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_SubNzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_SubNzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.Exports.join_GRing_SubNzRing_between_GRing_SubNzSemiRing_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzRing_isSubUnitRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubNzRing_isSubUnitRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiAlgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_NzSemiRing_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubNzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubNzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_SubNzLSemiAlgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.Exports.join_GRing_SubNzSemiAlgebra_between_GRing_SubNzSemiRing_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.join_GRing_SubNzSemiRing_between_GRing_NzSemiRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.join_GRing_SubNzSemiRing_between_GRing_NzSemiRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.join_GRing_SubNzSemiRing_between_GRing_NzSemiRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.join_GRing_SubNzSemiRing_between_GRing_NzSemiRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.join_GRing_SubNzSemiRing_between_GRing_NzSemiRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.join_GRing_SubNzSemiRing_between_GRing_NzSemiRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.Exports.join_GRing_SubNzSemiRing_between_GRing_NzSemiRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubNzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_Algebra_BaseZmodule_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_Lmodule_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzAlgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzLalgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzRing_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubPzLalgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_SubLmodule_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_SubPzLalgebra_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_SubPzRing_and_GRing_SubPzSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_SubPzSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.Exports.join_GRing_SubPzAlgebra_between_GRing_SubPzSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_Algebra_BaseZmodule_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_Lmodule_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_Lmodule_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_Lmodule_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_LSemiModule_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLalgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLSemiAlgebra_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzLSemiAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzRing_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzRing_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzRing_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_PzSemiRing_and_GRing_SubLmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_SubLmodule_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_SubLmodule_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_SubLmodule_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_SubLSemiModule_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_SubPzLSemiAlgebra_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_SubPzLSemiAlgebra_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.Exports.join_GRing_SubPzLalgebra_between_GRing_SubPzLSemiAlgebra_and_GRing_SubPzRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLalgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_LSemiModule_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzLSemiAlgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_PzSemiRing_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.Exports.join_GRing_SubPzLSemiAlgebra_between_GRing_SubLSemiModule_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzLSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_Algebra_BaseZmodule_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzRing_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_PzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_SubPzSemiRing_and_Algebra_SubZmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.Exports.join_GRing_SubPzRing_between_GRing_SubPzSemiRing_and_Algebra_Zmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzRing_isSubComPzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubPzRing_isSubComPzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubLSemiModule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubPzLSemiAlgebra [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.Exports.join_GRing_SubPzSemiAlgebra_between_GRing_PzSemiAlgebra_and_GRing_SubPzSemiRing [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.Exports.join_GRing_SubPzSemiRing_between_GRing_PzSemiRing_and_Algebra_SubAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.Exports.join_GRing_SubPzSemiRing_between_GRing_PzSemiRing_and_Algebra_SubBaseAddUMagma [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.Exports.join_GRing_SubPzSemiRing_between_GRing_PzSemiRing_and_Algebra_SubNmodule [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.Exports.join_GRing_SubPzSemiRing_between_GRing_PzSemiRing_and_choice_SubChoice [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.Exports.join_GRing_SubPzSemiRing_between_GRing_PzSemiRing_and_eqtype_SubEquality [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.Exports.join_GRing_SubPzSemiRing_between_GRing_PzSemiRing_and_eqtype_SubType [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing_isNonZero.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubPzSemiRing_isNonZero.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subr_2closed [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.subring_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubRing_SubLmodule_isSubLalgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubRing_SubLmodule_isSubLalgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_Algebra_AddClosed_and_GRing_SmulClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_Algebra_OppClosed_and_GRing_Semiring2Closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_Algebra_OppClosed_and_GRing_SemiringClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_GRing_Mul2Closed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_GRing_MulClosed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_GRing_Semiring2Closed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_GRing_Semiring2Closed_and_GRing_SmulClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_GRing_SemiringClosed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_GRing_SemiringClosed_and_GRing_SmulClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.Exports.join_GRing_SubringClosed_between_GRing_SmulClosed_and_Algebra_ZmodClosed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubringClosed.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemialg_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemimod_closed [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_isSubComSemiRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_isSubComSemiRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_SubLSemiModule_isSubLSemiAlgebra.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubSemiRing_SubLSemiModule_isSubLSemiAlgebra.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_Algebra_SubAddUMagma_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_Algebra_SubBaseAddUMagma_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_Algebra_SubNmodule_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_Algebra_SubZmodule_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_choice_SubChoice_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_eqtype_SubEquality_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_eqtype_SubType_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_GRing_SubNzRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_GRing_SubNzSemiRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_GRing_SubPzRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.Exports.join_GRing_SubUnitRing_between_GRing_SubPzSemiRing_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.SubUnitRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.add0r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addf_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.addIr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.additive [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.additive_linear [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.additive_semilinear [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.addKr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addKr_char2 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.addKr_pchar2 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addNKr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addNr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addr0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addr0_eq [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addr_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrAC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrACA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrCA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrI [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrK [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrK_char2 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.addrK_pchar2 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrKA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrNK [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.addrr_char2 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.addrr_pchar2 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.bin_lt_charf_0 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.bin_lt_pcharf_0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.can2_additive [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.can2_linear [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.can2_monoid_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.can2_nmod_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.can2_rmorphism [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.can2_scalable [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.can2_semi_additive [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.can2_semilinear [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.can2_zmod_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.char0_natf_div [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.char_lalg [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.charf'_nat [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.charf0 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.charf0P [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.charf_eq [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.charf_prime [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.comm_alg [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr_prod [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr_refl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr_sign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commr_sym [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commrB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commrD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commrM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commrMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commrN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commrN1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.commrV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.commrX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.div1r [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divff [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divfI [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divfK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divIf [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divIr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divKf [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divKr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divr1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divr1_eq [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divr_signM [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divrI [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divringClosedP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divrK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divrN [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divrNN [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.divrr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.dvdn_charf [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.dvdn_pcharf [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.eq_eval [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.eq_holds [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.eq_sat [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.eq_sol [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.eqf_sqr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.eqr_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.eqr_opp [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.eqr_oppLR [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.eqr_sum_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.eval_tsubst [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.expf_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.expf_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.expfB [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.expfB_cond [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.expfS_eq1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.expr0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.expr0n [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.expr1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.expr1n [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.expr2 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.expr_div_n [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.expr_dvd [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.expr_mod [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.expr_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprAC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprB [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.exprBn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprBn_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprD1n [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprDn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprDn_char [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.exprDn_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprDn_pchar [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprMn_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprMn_n [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprNn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprNn_char [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.exprNn_pchar [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprS [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprSr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.exprVn [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.exprZn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.fieldP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorph_char [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.fmorph_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorph_eq [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorph_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorph_eq1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorph_inj [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorph_pchar [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorph_unit [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fmorphV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fpred_divl [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fpred_divr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fpredMl [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.fpredMr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.Frobenius_aut0 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_aut1 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_aut_nat [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_autB_comm [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_autD_comm [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_autE [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_autM_comm [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_autMn [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_autN [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.Frobenius_autX [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.holds_fsubst [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.imaginary_exists [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.in_algE [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.invf_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invfM [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr_eq1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr_inj [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr_out [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr_sign [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invr_signM [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invrK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invrM [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invrN [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invrN1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.invrZ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.iter_addr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.iter_addr_0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.iter_mulr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.iter_mulr_1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linear0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linear_for [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linear_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearE [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearMNn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearPZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearZ_LR [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.linearZZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.lreg1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.lreg_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.lreg_sign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.lregM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.lregN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.lregP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.lregX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.monoid_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mul0r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mul0rn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mul1r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulf_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulf_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulf_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulfI [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulfK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulfV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulfVK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulIf [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulIr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulIr0_rreg [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulIr_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulKf [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulKr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulN1r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulNr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulNrn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr0n [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr1_eq [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulr1n [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr2n [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_algl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_algr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_natl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_natr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_sign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_signM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_suml [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulr_sumr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrAC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrACA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrb [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrBl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrBr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrCA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrDl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrI [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulrI0_lreg [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrI_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulrN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrN1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrn_char [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.mulrn_pchar [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnAC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnAl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnAr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnBl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnBr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnDl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrnDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrNN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrS [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrSr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.mulrV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulrVK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.multiplicative [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.mulVf [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulVKf [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulVKr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.mulVr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.nat1r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.natf0_char [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.natf0_pchar [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.natf_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.natf_neq0_pchar [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.natr1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.natr_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.natr_prod [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.natr_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.natrB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.natrD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.natrM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.natrX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.nmod_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.nmod_morphism_semilinear [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.oner_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.oner_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.oppr0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.oppr_char2 [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.oppr_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.oppr_inj [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.oppr_pchar2 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.opprB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.opprD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.opprK [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pchar0_natf_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.pchar_lalg [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.pcharf'_nat [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.pcharf0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pcharf0P [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.pcharf_eq [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pcharf_prime [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_aut0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_aut1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_aut_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_autB_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_autD_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_autE [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_autM_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_autMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_autN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.pFrobenius_autX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodf_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.prodf_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.prodf_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.prodf_seq_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.prodf_seq_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.prodfV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.prodr_const [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodr_const_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodr_undup_exp_count [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrM_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrMl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrMl_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrMn_const [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrMr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrMr_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.prodrXl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.prodrXr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddf [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddf0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddf_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddf_inj [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddf_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfMnat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfMNn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfMsign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfZnat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.raddfZsign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rev_prodr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rev_prodrV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rev_unitrP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.revrX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_alg [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_char [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.rmorph_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rmorph_eq1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_eq_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_pchar [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_prod [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_sign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorph_unit [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rmorphB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphE [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphism_monoidP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphismMP [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.rmorphM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphMNn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphMsign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphN1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rmorphV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rmorphXn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred0D [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred1M [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred_div [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpred_divl [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpred_divr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpred_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred_prod [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred_sign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpred_sum [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredBC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredBl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredBr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredDl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredMl [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpredMn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredMNn [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredMr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpredMsign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredN1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredNr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpredVr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpredX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredXN [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpredZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredZeq [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rpredZnat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rpredZsign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rreg1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rreg_neq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rregM [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rregN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.rregP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.rregX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.satP [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.scalable_for [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalable_linear [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalable_semilinear [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalarP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalarZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scale0r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scale1r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaleN1r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaleNr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.scaler_injl [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.scaler_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_prod [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_prodl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_prodr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_sign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_suml [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_sumr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scaler_unit [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.scalerA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerAl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerAr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerBl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerBr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerCA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerDl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerDr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerI [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.scalerK [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.scalerKV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.scalerMnl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerMnr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.scalerN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.semi_additive [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Theory.semilinear_for [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.semilinearP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.semilinearPZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.semiringClosedP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.semiscalarP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.signr_addb [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.signr_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.signr_odd [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.signrE [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.signrMK [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.signrN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.signrZK [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.size_sol [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.solP [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.solve_monicpoly [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.Theory.sqrf_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.sqrf_eq1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.sqrr_sign [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sqrrB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sqrrB1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sqrrD [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sqrrD1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sqrrN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sub0r [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subalgClosedP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subIr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subKr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.submodClosedP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subr0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subr0_eq [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subr_eq [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subr_eq0 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subr_sqr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subr_sqr_1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subr_sqrDB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrI [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subringClosedP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrK [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrKA [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrKC [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrX1 [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrXX [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.subrXX_comm [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sumr_const [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sumr_const_nat [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sumrB [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sumrMnl [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sumrMnr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.sumrN [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.telescope_prodf [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.telescope_prodf_eq [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.telescope_prodr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.telescope_prodr_eq [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.telescope_sumr [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.telescope_sumr_eq [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.unitfE [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitr0 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitr1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitr_prod [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitr_prod_in [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitr_prodP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrE [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrM [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrM_comm [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrMl [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrMr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrN [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrN1 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrP [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrPr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrV [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrX [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.unitrX_pos [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Theory.zmod_morphism [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.zmod_morphism_linear [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Theory.zmodClosedP [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.to_rform [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.to_rterm [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.tsubst [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.ub_var [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.unit [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unit_pred [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unit_subdef [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_Lmodule_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_LSemiModule_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_NzAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_NzLalgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_NzLSemiAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_NzSemiAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_PzAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_PzLalgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_PzLSemiAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.Exports.join_GRing_UnitAlgebra_between_GRing_PzSemiAlgebra_and_GRing_UnitRing [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitAlgebra.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.pack_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.phant_clone [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing.phant_on_ [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing_isField.identity_builder [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing_isField.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.UnitRing_isField.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.valid_QE_proj [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.valZ [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.wf_QE_proj [def, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.zmod_closedD [def, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.Zmodule_isComNzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComNzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComPzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isComPzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isLmodule.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isLmodule.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isNzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isNzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isPzRing.phant_axioms [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Zmodule_isPzRing.phant_Build [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
gring_class_sum [def, in mathcomp.group_representation.integral_char]
gring_classM_coef [def, in mathcomp.group_representation.integral_char]
gring_classM_coef_set [def, in mathcomp.group_representation.integral_char]
gring_index [def, in mathcomp.group_representation.mxrepresentation]
gring_irr_mode.body [def, in mathcomp.group_representation.integral_char]
gring_irr_mode.unlock [def, in mathcomp.group_representation.integral_char]
gring_irr_mode_unlock_subterm [def, in mathcomp.group_representation.integral_char]
gring_irr_mode_unlockable [def, in mathcomp.group_representation.integral_char]
gring_mx [def, in mathcomp.group_representation.mxrepresentation]
gring_op [def, in mathcomp.group_representation.mxrepresentation]
gring_proj [def, in mathcomp.group_representation.mxrepresentation]
gring_row [def, in mathcomp.group_representation.mxrepresentation]
group [def, in mathcomp.finite_group.fingroup]
Group.pack_ [def, in mathcomp.boot.monoid]
Group.phant_clone [def, in mathcomp.boot.monoid]
Group.phant_on_ [def, in mathcomp.boot.monoid]
group_closed [def, in mathcomp.boot.monoid]
group_closure_field [def, in mathcomp.group_representation.mxrepresentation]
group_dfwith [def, in mathcomp.finite_group.gproduct]
group_of [def, in mathcomp.finite_group.fingroup]
group_rel_of [def, in mathcomp.solvable.gseries]
group_ring [def, in mathcomp.group_representation.mxrepresentation]
group_set [def, in mathcomp.finite_group.fingroup]
group_splitting_field [def, in mathcomp.group_representation.mxrepresentation]
GroupClosed.Exports.join_monoid_GroupClosed_between_monoid_InvClosed_and_monoid_MulClosed [def, in mathcomp.boot.monoid]
GroupClosed.Exports.join_monoid_GroupClosed_between_monoid_InvClosed_and_monoid_UMagmaClosed [def, in mathcomp.boot.monoid]
GroupClosed.pack_ [def, in mathcomp.boot.monoid]
GroupClosed.phant_clone [def, in mathcomp.boot.monoid]
GroupClosed.phant_on_ [def, in mathcomp.boot.monoid]
GroupSet.sort [def, in mathcomp.finite_group.fingroup]
GroupSetBaseGroupSig.sort [def, in mathcomp.finite_group.fingroup]
GroupSetFinStarMonoidSig.sort [def, in mathcomp.finite_group.fingroup]
GroupSetMagmaSig.sort [def, in mathcomp.finite_group.fingroup]
groupXn1 [def, in mathcomp.finite_group.gproduct]
gset_mx [def, in mathcomp.group_representation.mxrepresentation]
gsimp [def, in mathcomp.boot.monoid]
gtn [def, in mathcomp.boot.ssrnat]
gX [def, in mathcomp.field.qfpoly]