diff options
| author | Cyril Cohen | 2019-04-08 14:18:00 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-08 14:18:00 +0200 |
| commit | 86d0a640383d6039302b9126620d0bf031a2a011 (patch) | |
| tree | f81a6cfe987fcd2944f9df1566a6059408761cf6 | |
| parent | 8099c05ca650b12abd0fbaf676357e86fd175a8a (diff) | |
| parent | a348deb229074be37ff31fd892a7d8835a49b566 (diff) | |
Merge pull request #318 from CohenCyril/hierarchy_test
Least common childen
| -rwxr-xr-x | etc/utils/hierarchy-diagram | 38 | ||||
| -rw-r--r-- | etc/utils/hierarchy_test.py | 90 | ||||
| -rw-r--r-- | mathcomp/algebra/finalg.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 3 | ||||
| -rw-r--r-- | mathcomp/test_suite/hierarchy_test.v | 2197 |
5 files changed, 1581 insertions, 757 deletions
diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram index 845ecfa..e30bb87 100755 --- a/etc/utils/hierarchy-diagram +++ b/etc/utils/hierarchy-diagram @@ -40,6 +40,7 @@ raw_coercions=$(tempfile -s .out | sed s/\.out$//) raw_canonicals=$(tempfile -s .out | sed s/\.out$//) parsed_coercions=$(tempfile) parsed_canonicals=$(tempfile) +opt_raw_inheritances=off opt_canonicals=on opt_coercions=off opt_libs=() @@ -49,6 +50,10 @@ while [[ $# -gt 0 ]] do case "$1" in + -raw-inheritances) + opt_raw_inheritances=on + shift; + ;; -canonicals) opt_canonicals="$2" shift; shift @@ -86,18 +91,31 @@ Redirect "$raw_coercions" Print Graph. Redirect "$raw_canonicals" Print Canonical Projections. EOT +cat $raw_canonicals.out \ +| sed -n 's/^\([a-zA-Z_\.]*\)\.sort <- \([a-zA-Z_\.]*\)\.sort ( \([a-zA-Z_\.]*\)\.\([a-zA-Z_]*\) )$/\1 \2 \3 \4/p' \ +| while read -r from_module to_module proj_module projection; do + if [[ $from_module = $proj_module ]] || [[ $to_module = $proj_module ]]; then + echo $from_module $to_module $proj_module $projection + fi +done > $parsed_canonicals + +cat $raw_coercions.out \ +| sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions + +if [[ $opt_raw_inheritances != "off" ]]; then + + cat $parsed_canonicals | sed 's/^\([^ ]*\) \([^ ]*\) .*$/\1\n\2/g' | sort | uniq \ + | while read -r module; do + echo -n "$module " + sed -n "s/^\([^ ]*\) $module .*$/\1/p" $parsed_canonicals | sort | xargs + done + +else + echo "digraph structures {" if [[ $opt_canonicals != "off" ]]; then - cat $raw_canonicals.out \ - | sed -n 's/^\([a-zA-Z_\.]*\)\.sort <- \([a-zA-Z_\.]*\)\.sort ( \([a-zA-Z_\.]*\)\.\([a-zA-Z_]*\) )$/\1 \2 \3 \4/p' \ - | while read -r from_module to_module proj_module projection; do - if [[ $from_module = $proj_module ]] || [[ $to_module = $proj_module ]]; then - echo $from_module $to_module $proj_module $projection - fi - done > $parsed_canonicals - cat $parsed_canonicals | while read -r from_module to_module proj_module projection; do grep "^$from_module " $parsed_canonicals | ( while read -r _ middle_module _ _; do if grep -q "^$middle_module $to_module " $parsed_canonicals; then @@ -114,8 +132,6 @@ if [[ $opt_canonicals != "off" ]]; then fi if [[ $opt_coercions != "off" ]]; then - cat $raw_coercions.out \ - | sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions cat $parsed_coercions | while read -r from_module to_module coercion; do grep "^$from_module " $parsed_coercions | ( while read -r _ middle_module _; do @@ -133,4 +149,6 @@ fi echo "}" +fi + rm $raw_coercions.out $raw_canonicals.out $parsed_coercions $parsed_canonicals diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py index 79e065c..b0a034c 100644 --- a/etc/utils/hierarchy_test.py +++ b/etc/utils/hierarchy_test.py @@ -1,45 +1,79 @@ #!/usr/bin/python # usage: hiearchy_test.py inputfile -import pygraphviz as pgv -import sys, argparse +import sys, argparse, collections -def children(G,n): - res = set() - new = set([n]) - while new != set(): - p = new.pop() - res.add(p) - new.update(set(G.successors(p)).difference(res)) - return res +def print_hierarchy_test(G, test_cases): + print ("(** Generated by etc/utils/hierarchy_test.py *)") + print ("From mathcomp Require Import all.") -def common_children(G): - result = set() - for x in G.nodes(): - for y in G.nodes(): - if x < y and children(G,x).intersection(children(G,y)) != set(): - result.add((x,y)) - return result - -def print_common_children_coq_check(G): - print("(** Generated by etc/utils/hierarchy_test.py *)") - print("From mathcomp Require Import all.") - for x in G.nodes(): + print (""" +(* `check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`. *) +Tactic Notation "check_join" + open_constr(t1) open_constr(t2) open_constr(tjoin) := + let T1 := open_constr:(_ : t1) in + let T2 := open_constr:(_ : t2) in + match tt with + | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2) + | _ => fail "There is no join of" t1 "and" t2 + end; + let Tjoin := + lazymatch T1 with + | _ (_ ?Tjoin) => constr: (Tjoin) + | _ ?Tjoin => constr: (Tjoin) + | ?Tjoin => constr: (Tjoin) + end + in + is_evar Tjoin; + let tjoin' := type of Tjoin in + lazymatch tjoin' with + | tjoin => lazymatch tjoin with + | tjoin' => idtac + | _ => idtac tjoin' + end + | _ => fail "The join of" t1 "and" t2 "is" tjoin' + "but is expected to be" tjoin + end. +""") + for x in G.keys(): if x.rfind("Lmod") >= 0 or x.rfind("Splitting") >= 0 or \ x.rfind("lgebra") >= 0 or x.rfind("FieldExt") >= 0 or \ x.rfind("Vector") >= 0: - print ("Local Notation \"" + x + ".type\" := (" + x + ".type _).") + print ("Local Notation \"" + x + ".type\" := (" + x + ".type _) (only parsing).") print ("") - for (x, y) in common_children(G): - print ("Goal False. have := erefl : (_ : " + x + ".type) = (_ : " + y + ".type) :> Type. Abort.") + print ("Goal False.") + for (x,y,z) in test_cases: + print ("check_join " + x + ".type " + y + ".type " + z + ".type.") + print ("Abort.") + +def compute_least_common_children(G): + tests=[] + for pa, ch_a in G.items(): + for pb, ch_b in G.items(): + ch_c = ({pa} | ch_a) & ({pb} | ch_b) # common children + for c in ch_c: + ch_c = ch_c - G[c] + if len(ch_c) == 1: + tests.append((pa, pb, ch_c.pop())) + elif 2 <= len(ch_c): + print (pa, "and", pb, "have more than two least common children:", ch_c, ".", file=sys.stderr) + sys.exit(1) + return tests def main(): parser = argparse.ArgumentParser(description='Generate a check .v file \ for mathcomp structure hiearchies') - parser.add_argument('dotfile', metavar='<dotfile>', nargs=1, - help='a dotfile representing the hierarchy') + parser.add_argument('graph', metavar='<graph>', nargs=1, + help='a file representing the hierarchy') args = parser.parse_args() - print_common_children_coq_check(pgv.AGraph(args.dotfile[0])) + G = {} + with open(args.graph[0]) as f: + for line in f: + words = line.split() + p = words.pop(0) + G[p] = set(words) + G = collections.OrderedDict(sorted(G.items())) + print_hierarchy_test(G, compute_least_common_children(G)) if __name__ == "__main__": main() diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index ac3a74e..9c0025b 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -125,7 +125,9 @@ Coercion countType : type >-> Countable.type. Canonical countType. Coercion finType : type >-> Finite.type. Canonical finType. +Coercion baseFinGroupType : type >-> FinGroup.base_type. Canonical baseFinGroupType. +Coercion finGroupType : type >-> FinGroup.type. Canonical finGroupType. Coercion zmodType : type >-> GRing.Zmodule.type. Canonical zmodType. @@ -645,13 +647,9 @@ Definition countComUnitRing_finComRingType := @ComRing.Pack countComUnitRingType xclass. Definition countComUnitRing_finUnitRingType := @UnitRing.Pack countComUnitRingType xclass. -Definition unitRing_countComRingType := - @CountRing.ComRing.Pack unitRingType xclass. Definition unitRing_finComRingType := @ComRing.Pack unitRingType xclass. Definition countUnitRing_finComRingType := @ComRing.Pack countUnitRingType xclass. -Definition comRing_countUnitRingType := - @CountRing.UnitRing.Pack comRingType xclass. Definition comRing_finUnitRingType := @UnitRing.Pack comRingType xclass. Definition countComRing_finUnitRingType := @UnitRing.Pack countComRingType xclass. @@ -720,10 +718,8 @@ Canonical countComUnitRing_finZmodType. Canonical countComUnitRing_finRingType. Canonical countComUnitRing_finComRingType. Canonical countComUnitRing_finUnitRingType. -Canonical unitRing_countComRingType. Canonical unitRing_finComRingType. Canonical countUnitRing_finComRingType. -Canonical comRing_countUnitRingType. Canonical comRing_finUnitRingType. Canonical countComRing_finUnitRingType. Canonical finComRing_finUnitRingType. @@ -1231,7 +1227,6 @@ Definition lalg_finZmodType := @Zmodule.Pack lalgType xclass. Definition lalg_finLmodType := @Lmodule.Pack R phR lalgType xclass. Definition lalg_countRingType := @CountRing.Ring.Pack lalgType xclass. Definition lalg_finRingType := @Ring.Pack lalgType xclass. -Definition lmod_ringType := @GRing.Ring.Pack lmodType xclass. Definition lmod_countRingType := @CountRing.Ring.Pack lmodType xclass. Definition lmod_finRingType := @Ring.Pack lmodType xclass. Definition finLmod_ringType := @GRing.Ring.Pack finLmodType xclass. @@ -1285,7 +1280,6 @@ Canonical lalg_finZmodType. Canonical lalg_finLmodType. Canonical lalg_countRingType. Canonical lalg_finRingType. -Canonical lmod_ringType. Canonical lmod_countRingType. Canonical lmod_finRingType. Canonical finLmod_ringType. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 9ac5236..a51fe9c 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -1533,7 +1533,8 @@ Canonical extremal_group_countType := CountType _ extremal_group_countMixin. Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6. Proof. by case: c. Qed. Definition extremal_group_finMixin := Finite.CountMixin bound_extremal_groups. -Canonical extremal_group_finType := FinType _ extremal_group_finMixin. +Canonical extremal_group_finType := + FinType extremal_group_type extremal_group_finMixin. Definition extremal_class (A : {set gT}) := let m := #|A| in let p := pdiv m in let n := logn p m in diff --git a/mathcomp/test_suite/hierarchy_test.v b/mathcomp/test_suite/hierarchy_test.v index e806362..5ea8980 100644 --- a/mathcomp/test_suite/hierarchy_test.v +++ b/mathcomp/test_suite/hierarchy_test.v @@ -1,713 +1,1490 @@ (** Generated by etc/utils/hierarchy_test.py *) From mathcomp Require Import all. -Local Notation "FinRing.UnitAlgebra.type" := (FinRing.UnitAlgebra.type _). -Local Notation "GRing.Lalgebra.type" := (GRing.Lalgebra.type _). -Local Notation "FinRing.Lalgebra.type" := (FinRing.Lalgebra.type _). -Local Notation "FinRing.Algebra.type" := (FinRing.Algebra.type _). -Local Notation "FieldExt.type" := (FieldExt.type _). -Local Notation "GRing.UnitAlgebra.type" := (GRing.UnitAlgebra.type _). -Local Notation "FinRing.Lmodule.type" := (FinRing.Lmodule.type _). -Local Notation "GRing.Algebra.type" := (GRing.Algebra.type _). -Local Notation "SplittingField.type" := (SplittingField.type _). -Local Notation "Falgebra.type" := (Falgebra.type _). -Local Notation "GRing.Lmodule.type" := (GRing.Lmodule.type _). -Local Notation "Vector.type" := (Vector.type _). -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : FieldExt.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Falgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FieldExt.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.ClosedField.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : SplittingField.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Falgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.NumField.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.ClosedField.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FieldExt.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : CountRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.RealDomain.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : Countable.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Lmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.NumField.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : Finite.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : Equality.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Lalgebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Vector.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Field.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Num.NumField.type) = (_ : Num.RealDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : SplittingField.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.DecidableField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinGroup.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Zmodule.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.Ring.type) :> Type. Abort. -Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.ClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type. Abort. -Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.ComRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort. -Goal False. have := erefl : (_ : Equality.type) = (_ : Num.RealClosedField.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort. -Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort. +(* `check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`. *) +Tactic Notation "check_join" + open_constr(t1) open_constr(t2) open_constr(tjoin) := + let T1 := open_constr:(_ : t1) in + let T2 := open_constr:(_ : t2) in + match tt with + | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2) + | _ => fail "There is no join of" t1 "and" t2 + end; + let Tjoin := + lazymatch T1 with + | _ (_ ?Tjoin) => constr: (Tjoin) + | _ ?Tjoin => constr: (Tjoin) + | ?Tjoin => constr: (Tjoin) + end + in + is_evar Tjoin; + let tjoin' := type of Tjoin in + lazymatch tjoin' with + | tjoin => lazymatch tjoin with + | tjoin' => idtac + | _ => idtac tjoin' + end + | _ => fail "The join of" t1 "and" t2 "is" tjoin' + "but is expected to be" tjoin + end. + +Local Notation "Falgebra.type" := (Falgebra.type _) (only parsing). +Local Notation "FieldExt.type" := (FieldExt.type _) (only parsing). +Local Notation "FinRing.Algebra.type" := (FinRing.Algebra.type _) (only parsing). +Local Notation "FinRing.Lalgebra.type" := (FinRing.Lalgebra.type _) (only parsing). +Local Notation "FinRing.Lmodule.type" := (FinRing.Lmodule.type _) (only parsing). +Local Notation "FinRing.UnitAlgebra.type" := (FinRing.UnitAlgebra.type _) (only parsing). +Local Notation "GRing.Algebra.type" := (GRing.Algebra.type _) (only parsing). +Local Notation "GRing.Lalgebra.type" := (GRing.Lalgebra.type _) (only parsing). +Local Notation "GRing.Lmodule.type" := (GRing.Lmodule.type _) (only parsing). +Local Notation "GRing.UnitAlgebra.type" := (GRing.UnitAlgebra.type _) (only parsing). +Local Notation "SplittingField.type" := (SplittingField.type _) (only parsing). +Local Notation "Vector.type" := (Vector.type _) (only parsing). + +Goal False. +check_join Choice.type Choice.type Choice.type. +check_join Choice.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join Choice.type CountRing.ComRing.type CountRing.ComRing.type. +check_join Choice.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join Choice.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join Choice.type CountRing.Field.type CountRing.Field.type. +check_join Choice.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join Choice.type CountRing.Ring.type CountRing.Ring.type. +check_join Choice.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join Choice.type CountRing.Zmodule.type CountRing.Zmodule.type. +check_join Choice.type Countable.type Countable.type. +check_join Choice.type Equality.type Choice.type. +check_join Choice.type Falgebra.type Falgebra.type. +check_join Choice.type FieldExt.type FieldExt.type. +check_join Choice.type FinGroup.type FinGroup.type. +check_join Choice.type FinRing.Algebra.type FinRing.Algebra.type. +check_join Choice.type FinRing.ComRing.type FinRing.ComRing.type. +check_join Choice.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join Choice.type FinRing.Field.type FinRing.Field.type. +check_join Choice.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join Choice.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join Choice.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join Choice.type FinRing.Ring.type FinRing.Ring.type. +check_join Choice.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join Choice.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join Choice.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join Choice.type Finite.type Finite.type. +check_join Choice.type GRing.Algebra.type GRing.Algebra.type. +check_join Choice.type GRing.ClosedField.type GRing.ClosedField.type. +check_join Choice.type GRing.ComRing.type GRing.ComRing.type. +check_join Choice.type GRing.ComUnitRing.type GRing.ComUnitRing.type. +check_join Choice.type GRing.DecidableField.type GRing.DecidableField.type. +check_join Choice.type GRing.Field.type GRing.Field.type. +check_join Choice.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join Choice.type GRing.Lalgebra.type GRing.Lalgebra.type. +check_join Choice.type GRing.Lmodule.type GRing.Lmodule.type. +check_join Choice.type GRing.Ring.type GRing.Ring.type. +check_join Choice.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join Choice.type GRing.UnitRing.type GRing.UnitRing.type. +check_join Choice.type GRing.Zmodule.type GRing.Zmodule.type. +check_join Choice.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join Choice.type Num.ClosedField.type Num.ClosedField.type. +check_join Choice.type Num.NumDomain.type Num.NumDomain.type. +check_join Choice.type Num.NumField.type Num.NumField.type. +check_join Choice.type Num.RealClosedField.type Num.RealClosedField.type. +check_join Choice.type Num.RealDomain.type Num.RealDomain.type. +check_join Choice.type Num.RealField.type Num.RealField.type. +check_join Choice.type SplittingField.type SplittingField.type. +check_join Choice.type Vector.type Vector.type. +check_join CountRing.ClosedField.type Choice.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.ComRing.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.ComUnitRing.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.DecidableField.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.Field.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.IntegralDomain.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.Ring.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.UnitRing.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type CountRing.Zmodule.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type Countable.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type Equality.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.ComRing.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.ComUnitRing.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.DecidableField.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.Field.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.IntegralDomain.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.Ring.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.UnitRing.type CountRing.ClosedField.type. +check_join CountRing.ClosedField.type GRing.Zmodule.type CountRing.ClosedField.type. +check_join CountRing.ComRing.type Choice.type CountRing.ComRing.type. +check_join CountRing.ComRing.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.ComRing.type CountRing.ComRing.type CountRing.ComRing.type. +check_join CountRing.ComRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComRing.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.ComRing.type CountRing.Field.type CountRing.Field.type. +check_join CountRing.ComRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.ComRing.type CountRing.Ring.type CountRing.ComRing.type. +check_join CountRing.ComRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComRing.type CountRing.Zmodule.type CountRing.ComRing.type. +check_join CountRing.ComRing.type Countable.type CountRing.ComRing.type. +check_join CountRing.ComRing.type Equality.type CountRing.ComRing.type. +check_join CountRing.ComRing.type FinGroup.type FinRing.ComRing.type. +check_join CountRing.ComRing.type FinRing.ComRing.type FinRing.ComRing.type. +check_join CountRing.ComRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join CountRing.ComRing.type FinRing.Field.type FinRing.Field.type. +check_join CountRing.ComRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join CountRing.ComRing.type FinRing.Ring.type FinRing.ComRing.type. +check_join CountRing.ComRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type. +check_join CountRing.ComRing.type FinRing.Zmodule.type FinRing.ComRing.type. +check_join CountRing.ComRing.type Finite.type FinRing.ComRing.type. +check_join CountRing.ComRing.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.ComRing.type GRing.ComRing.type CountRing.ComRing.type. +check_join CountRing.ComRing.type GRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComRing.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.ComRing.type GRing.Field.type CountRing.Field.type. +check_join CountRing.ComRing.type GRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.ComRing.type GRing.Ring.type CountRing.ComRing.type. +check_join CountRing.ComRing.type GRing.UnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComRing.type GRing.Zmodule.type CountRing.ComRing.type. +check_join CountRing.ComUnitRing.type Choice.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.ComUnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.ComUnitRing.type CountRing.Field.type CountRing.Field.type. +check_join CountRing.ComUnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.ComUnitRing.type CountRing.Ring.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type CountRing.Zmodule.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type Countable.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type Equality.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type FinGroup.type FinRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type FinRing.Field.type FinRing.Field.type. +check_join CountRing.ComUnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join CountRing.ComUnitRing.type FinRing.Ring.type FinRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type FinRing.Zmodule.type FinRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type Finite.type FinRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.ComUnitRing.type GRing.ComRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type GRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.ComUnitRing.type GRing.Field.type CountRing.Field.type. +check_join CountRing.ComUnitRing.type GRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.ComUnitRing.type GRing.Ring.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type GRing.UnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.ComUnitRing.type GRing.Zmodule.type CountRing.ComUnitRing.type. +check_join CountRing.DecidableField.type Choice.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.DecidableField.type CountRing.ComRing.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.ComUnitRing.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.Field.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.IntegralDomain.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.Ring.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.UnitRing.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type CountRing.Zmodule.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type Countable.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type Equality.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.DecidableField.type GRing.ComRing.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.ComUnitRing.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.Field.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.IntegralDomain.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.Ring.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.UnitRing.type CountRing.DecidableField.type. +check_join CountRing.DecidableField.type GRing.Zmodule.type CountRing.DecidableField.type. +check_join CountRing.Field.type Choice.type CountRing.Field.type. +check_join CountRing.Field.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.Field.type CountRing.ComRing.type CountRing.Field.type. +check_join CountRing.Field.type CountRing.ComUnitRing.type CountRing.Field.type. +check_join CountRing.Field.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.Field.type CountRing.Field.type CountRing.Field.type. +check_join CountRing.Field.type CountRing.IntegralDomain.type CountRing.Field.type. +check_join CountRing.Field.type CountRing.Ring.type CountRing.Field.type. +check_join CountRing.Field.type CountRing.UnitRing.type CountRing.Field.type. +check_join CountRing.Field.type CountRing.Zmodule.type CountRing.Field.type. +check_join CountRing.Field.type Countable.type CountRing.Field.type. +check_join CountRing.Field.type Equality.type CountRing.Field.type. +check_join CountRing.Field.type FinGroup.type FinRing.Field.type. +check_join CountRing.Field.type FinRing.ComRing.type FinRing.Field.type. +check_join CountRing.Field.type FinRing.ComUnitRing.type FinRing.Field.type. +check_join CountRing.Field.type FinRing.Field.type FinRing.Field.type. +check_join CountRing.Field.type FinRing.IntegralDomain.type FinRing.Field.type. +check_join CountRing.Field.type FinRing.Ring.type FinRing.Field.type. +check_join CountRing.Field.type FinRing.UnitRing.type FinRing.Field.type. +check_join CountRing.Field.type FinRing.Zmodule.type FinRing.Field.type. +check_join CountRing.Field.type Finite.type FinRing.Field.type. +check_join CountRing.Field.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.Field.type GRing.ComRing.type CountRing.Field.type. +check_join CountRing.Field.type GRing.ComUnitRing.type CountRing.Field.type. +check_join CountRing.Field.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.Field.type GRing.Field.type CountRing.Field.type. +check_join CountRing.Field.type GRing.IntegralDomain.type CountRing.Field.type. +check_join CountRing.Field.type GRing.Ring.type CountRing.Field.type. +check_join CountRing.Field.type GRing.UnitRing.type CountRing.Field.type. +check_join CountRing.Field.type GRing.Zmodule.type CountRing.Field.type. +check_join CountRing.IntegralDomain.type Choice.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.IntegralDomain.type CountRing.ComRing.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type CountRing.ComUnitRing.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.IntegralDomain.type CountRing.Field.type CountRing.Field.type. +check_join CountRing.IntegralDomain.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type CountRing.Ring.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type CountRing.UnitRing.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type CountRing.Zmodule.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type Countable.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type Equality.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type FinGroup.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type FinRing.ComRing.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type FinRing.ComUnitRing.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type FinRing.Field.type FinRing.Field.type. +check_join CountRing.IntegralDomain.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type FinRing.Ring.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type FinRing.UnitRing.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type FinRing.Zmodule.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type Finite.type FinRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.IntegralDomain.type GRing.ComRing.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type GRing.ComUnitRing.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.IntegralDomain.type GRing.Field.type CountRing.Field.type. +check_join CountRing.IntegralDomain.type GRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type GRing.Ring.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type GRing.UnitRing.type CountRing.IntegralDomain.type. +check_join CountRing.IntegralDomain.type GRing.Zmodule.type CountRing.IntegralDomain.type. +check_join CountRing.Ring.type Choice.type CountRing.Ring.type. +check_join CountRing.Ring.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.Ring.type CountRing.ComRing.type CountRing.ComRing.type. +check_join CountRing.Ring.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.Ring.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.Ring.type CountRing.Field.type CountRing.Field.type. +check_join CountRing.Ring.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.Ring.type CountRing.Ring.type CountRing.Ring.type. +check_join CountRing.Ring.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join CountRing.Ring.type CountRing.Zmodule.type CountRing.Ring.type. +check_join CountRing.Ring.type Countable.type CountRing.Ring.type. +check_join CountRing.Ring.type Equality.type CountRing.Ring.type. +check_join CountRing.Ring.type FinGroup.type FinRing.Ring.type. +check_join CountRing.Ring.type FinRing.Algebra.type FinRing.Algebra.type. +check_join CountRing.Ring.type FinRing.ComRing.type FinRing.ComRing.type. +check_join CountRing.Ring.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join CountRing.Ring.type FinRing.Field.type FinRing.Field.type. +check_join CountRing.Ring.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join CountRing.Ring.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join CountRing.Ring.type FinRing.Lmodule.type FinRing.Lalgebra.type. +check_join CountRing.Ring.type FinRing.Ring.type FinRing.Ring.type. +check_join CountRing.Ring.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.Ring.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join CountRing.Ring.type FinRing.Zmodule.type FinRing.Ring.type. +check_join CountRing.Ring.type Finite.type FinRing.Ring.type. +check_join CountRing.Ring.type GRing.Algebra.type FinRing.Algebra.type. +check_join CountRing.Ring.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.Ring.type GRing.ComRing.type CountRing.ComRing.type. +check_join CountRing.Ring.type GRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.Ring.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.Ring.type GRing.Field.type CountRing.Field.type. +check_join CountRing.Ring.type GRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.Ring.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join CountRing.Ring.type GRing.Lmodule.type FinRing.Lalgebra.type. +check_join CountRing.Ring.type GRing.Ring.type CountRing.Ring.type. +check_join CountRing.Ring.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.Ring.type GRing.UnitRing.type CountRing.UnitRing.type. +check_join CountRing.Ring.type GRing.Zmodule.type CountRing.Ring.type. +check_join CountRing.UnitRing.type Choice.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.UnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type. +check_join CountRing.UnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.UnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.UnitRing.type CountRing.Field.type CountRing.Field.type. +check_join CountRing.UnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.UnitRing.type CountRing.Ring.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type CountRing.Zmodule.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type Countable.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type Equality.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type FinGroup.type FinRing.UnitRing.type. +check_join CountRing.UnitRing.type FinRing.Algebra.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type. +check_join CountRing.UnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join CountRing.UnitRing.type FinRing.Field.type FinRing.Field.type. +check_join CountRing.UnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join CountRing.UnitRing.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type FinRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type FinRing.Ring.type FinRing.UnitRing.type. +check_join CountRing.UnitRing.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join CountRing.UnitRing.type FinRing.Zmodule.type FinRing.UnitRing.type. +check_join CountRing.UnitRing.type Finite.type FinRing.UnitRing.type. +check_join CountRing.UnitRing.type GRing.Algebra.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.UnitRing.type GRing.ComRing.type CountRing.ComUnitRing.type. +check_join CountRing.UnitRing.type GRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.UnitRing.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.UnitRing.type GRing.Field.type CountRing.Field.type. +check_join CountRing.UnitRing.type GRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.UnitRing.type GRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type GRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type GRing.Ring.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.UnitRing.type GRing.UnitRing.type CountRing.UnitRing.type. +check_join CountRing.UnitRing.type GRing.Zmodule.type CountRing.UnitRing.type. +check_join CountRing.Zmodule.type Choice.type CountRing.Zmodule.type. +check_join CountRing.Zmodule.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.Zmodule.type CountRing.ComRing.type CountRing.ComRing.type. +check_join CountRing.Zmodule.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.Zmodule.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.Zmodule.type CountRing.Field.type CountRing.Field.type. +check_join CountRing.Zmodule.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.Zmodule.type CountRing.Ring.type CountRing.Ring.type. +check_join CountRing.Zmodule.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join CountRing.Zmodule.type CountRing.Zmodule.type CountRing.Zmodule.type. +check_join CountRing.Zmodule.type Countable.type CountRing.Zmodule.type. +check_join CountRing.Zmodule.type Equality.type CountRing.Zmodule.type. +check_join CountRing.Zmodule.type FinGroup.type FinRing.Zmodule.type. +check_join CountRing.Zmodule.type FinRing.Algebra.type FinRing.Algebra.type. +check_join CountRing.Zmodule.type FinRing.ComRing.type FinRing.ComRing.type. +check_join CountRing.Zmodule.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join CountRing.Zmodule.type FinRing.Field.type FinRing.Field.type. +check_join CountRing.Zmodule.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join CountRing.Zmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join CountRing.Zmodule.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join CountRing.Zmodule.type FinRing.Ring.type FinRing.Ring.type. +check_join CountRing.Zmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.Zmodule.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join CountRing.Zmodule.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join CountRing.Zmodule.type Finite.type FinRing.Zmodule.type. +check_join CountRing.Zmodule.type GRing.Algebra.type FinRing.Algebra.type. +check_join CountRing.Zmodule.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join CountRing.Zmodule.type GRing.ComRing.type CountRing.ComRing.type. +check_join CountRing.Zmodule.type GRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join CountRing.Zmodule.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join CountRing.Zmodule.type GRing.Field.type CountRing.Field.type. +check_join CountRing.Zmodule.type GRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join CountRing.Zmodule.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join CountRing.Zmodule.type GRing.Lmodule.type FinRing.Lmodule.type. +check_join CountRing.Zmodule.type GRing.Ring.type CountRing.Ring.type. +check_join CountRing.Zmodule.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join CountRing.Zmodule.type GRing.UnitRing.type CountRing.UnitRing.type. +check_join CountRing.Zmodule.type GRing.Zmodule.type CountRing.Zmodule.type. +check_join Countable.type Choice.type Countable.type. +check_join Countable.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join Countable.type CountRing.ComRing.type CountRing.ComRing.type. +check_join Countable.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join Countable.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join Countable.type CountRing.Field.type CountRing.Field.type. +check_join Countable.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join Countable.type CountRing.Ring.type CountRing.Ring.type. +check_join Countable.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join Countable.type CountRing.Zmodule.type CountRing.Zmodule.type. +check_join Countable.type Countable.type Countable.type. +check_join Countable.type Equality.type Countable.type. +check_join Countable.type FinGroup.type FinGroup.type. +check_join Countable.type FinRing.Algebra.type FinRing.Algebra.type. +check_join Countable.type FinRing.ComRing.type FinRing.ComRing.type. +check_join Countable.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join Countable.type FinRing.Field.type FinRing.Field.type. +check_join Countable.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join Countable.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join Countable.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join Countable.type FinRing.Ring.type FinRing.Ring.type. +check_join Countable.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join Countable.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join Countable.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join Countable.type Finite.type Finite.type. +check_join Countable.type GRing.Algebra.type FinRing.Algebra.type. +check_join Countable.type GRing.ClosedField.type CountRing.ClosedField.type. +check_join Countable.type GRing.ComRing.type CountRing.ComRing.type. +check_join Countable.type GRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join Countable.type GRing.DecidableField.type CountRing.DecidableField.type. +check_join Countable.type GRing.Field.type CountRing.Field.type. +check_join Countable.type GRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join Countable.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join Countable.type GRing.Lmodule.type FinRing.Lmodule.type. +check_join Countable.type GRing.Ring.type CountRing.Ring.type. +check_join Countable.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join Countable.type GRing.UnitRing.type CountRing.UnitRing.type. +check_join Countable.type GRing.Zmodule.type CountRing.Zmodule.type. +check_join Equality.type Choice.type Choice.type. +check_join Equality.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join Equality.type CountRing.ComRing.type CountRing.ComRing.type. +check_join Equality.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join Equality.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join Equality.type CountRing.Field.type CountRing.Field.type. +check_join Equality.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join Equality.type CountRing.Ring.type CountRing.Ring.type. +check_join Equality.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join Equality.type CountRing.Zmodule.type CountRing.Zmodule.type. +check_join Equality.type Countable.type Countable.type. +check_join Equality.type Equality.type Equality.type. +check_join Equality.type Falgebra.type Falgebra.type. +check_join Equality.type FieldExt.type FieldExt.type. +check_join Equality.type FinGroup.type FinGroup.type. +check_join Equality.type FinRing.Algebra.type FinRing.Algebra.type. +check_join Equality.type FinRing.ComRing.type FinRing.ComRing.type. +check_join Equality.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join Equality.type FinRing.Field.type FinRing.Field.type. +check_join Equality.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join Equality.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join Equality.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join Equality.type FinRing.Ring.type FinRing.Ring.type. +check_join Equality.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join Equality.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join Equality.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join Equality.type Finite.type Finite.type. +check_join Equality.type GRing.Algebra.type GRing.Algebra.type. +check_join Equality.type GRing.ClosedField.type GRing.ClosedField.type. +check_join Equality.type GRing.ComRing.type GRing.ComRing.type. +check_join Equality.type GRing.ComUnitRing.type GRing.ComUnitRing.type. +check_join Equality.type GRing.DecidableField.type GRing.DecidableField.type. +check_join Equality.type GRing.Field.type GRing.Field.type. +check_join Equality.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join Equality.type GRing.Lalgebra.type GRing.Lalgebra.type. +check_join Equality.type GRing.Lmodule.type GRing.Lmodule.type. +check_join Equality.type GRing.Ring.type GRing.Ring.type. +check_join Equality.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join Equality.type GRing.UnitRing.type GRing.UnitRing.type. +check_join Equality.type GRing.Zmodule.type GRing.Zmodule.type. +check_join Equality.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join Equality.type Num.ClosedField.type Num.ClosedField.type. +check_join Equality.type Num.NumDomain.type Num.NumDomain.type. +check_join Equality.type Num.NumField.type Num.NumField.type. +check_join Equality.type Num.RealClosedField.type Num.RealClosedField.type. +check_join Equality.type Num.RealDomain.type Num.RealDomain.type. +check_join Equality.type Num.RealField.type Num.RealField.type. +check_join Equality.type SplittingField.type SplittingField.type. +check_join Equality.type Vector.type Vector.type. +check_join Falgebra.type Choice.type Falgebra.type. +check_join Falgebra.type Equality.type Falgebra.type. +check_join Falgebra.type Falgebra.type Falgebra.type. +check_join Falgebra.type FieldExt.type FieldExt.type. +check_join Falgebra.type GRing.Algebra.type Falgebra.type. +check_join Falgebra.type GRing.ComRing.type FieldExt.type. +check_join Falgebra.type GRing.ComUnitRing.type FieldExt.type. +check_join Falgebra.type GRing.Field.type FieldExt.type. +check_join Falgebra.type GRing.IntegralDomain.type FieldExt.type. +check_join Falgebra.type GRing.Lalgebra.type Falgebra.type. +check_join Falgebra.type GRing.Lmodule.type Falgebra.type. +check_join Falgebra.type GRing.Ring.type Falgebra.type. +check_join Falgebra.type GRing.UnitAlgebra.type Falgebra.type. +check_join Falgebra.type GRing.UnitRing.type Falgebra.type. +check_join Falgebra.type GRing.Zmodule.type Falgebra.type. +check_join Falgebra.type SplittingField.type SplittingField.type. +check_join Falgebra.type Vector.type Falgebra.type. +check_join FieldExt.type Choice.type FieldExt.type. +check_join FieldExt.type Equality.type FieldExt.type. +check_join FieldExt.type Falgebra.type FieldExt.type. +check_join FieldExt.type FieldExt.type FieldExt.type. +check_join FieldExt.type GRing.Algebra.type FieldExt.type. +check_join FieldExt.type GRing.ComRing.type FieldExt.type. +check_join FieldExt.type GRing.ComUnitRing.type FieldExt.type. +check_join FieldExt.type GRing.Field.type FieldExt.type. +check_join FieldExt.type GRing.IntegralDomain.type FieldExt.type. +check_join FieldExt.type GRing.Lalgebra.type FieldExt.type. +check_join FieldExt.type GRing.Lmodule.type FieldExt.type. +check_join FieldExt.type GRing.Ring.type FieldExt.type. +check_join FieldExt.type GRing.UnitAlgebra.type FieldExt.type. +check_join FieldExt.type GRing.UnitRing.type FieldExt.type. +check_join FieldExt.type GRing.Zmodule.type FieldExt.type. +check_join FieldExt.type SplittingField.type SplittingField.type. +check_join FieldExt.type Vector.type FieldExt.type. +check_join FinGroup.type Choice.type FinGroup.type. +check_join FinGroup.type CountRing.ComRing.type FinRing.ComRing.type. +check_join FinGroup.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinGroup.type CountRing.Field.type FinRing.Field.type. +check_join FinGroup.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinGroup.type CountRing.Ring.type FinRing.Ring.type. +check_join FinGroup.type CountRing.UnitRing.type FinRing.UnitRing.type. +check_join FinGroup.type CountRing.Zmodule.type FinRing.Zmodule.type. +check_join FinGroup.type Countable.type FinGroup.type. +check_join FinGroup.type Equality.type FinGroup.type. +check_join FinGroup.type FinGroup.type FinGroup.type. +check_join FinGroup.type FinRing.Algebra.type FinRing.Algebra.type. +check_join FinGroup.type FinRing.ComRing.type FinRing.ComRing.type. +check_join FinGroup.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinGroup.type FinRing.Field.type FinRing.Field.type. +check_join FinGroup.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinGroup.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinGroup.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join FinGroup.type FinRing.Ring.type FinRing.Ring.type. +check_join FinGroup.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinGroup.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join FinGroup.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join FinGroup.type Finite.type FinGroup.type. +check_join FinGroup.type GRing.Algebra.type FinRing.Algebra.type. +check_join FinGroup.type GRing.ComRing.type FinRing.ComRing.type. +check_join FinGroup.type GRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinGroup.type GRing.Field.type FinRing.Field.type. +check_join FinGroup.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinGroup.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinGroup.type GRing.Lmodule.type FinRing.Lmodule.type. +check_join FinGroup.type GRing.Ring.type FinRing.Ring.type. +check_join FinGroup.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinGroup.type GRing.UnitRing.type FinRing.UnitRing.type. +check_join FinGroup.type GRing.Zmodule.type FinRing.Zmodule.type. +check_join FinRing.Algebra.type Choice.type FinRing.Algebra.type. +check_join FinRing.Algebra.type CountRing.Ring.type FinRing.Algebra.type. +check_join FinRing.Algebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Algebra.type CountRing.Zmodule.type FinRing.Algebra.type. +check_join FinRing.Algebra.type Countable.type FinRing.Algebra.type. +check_join FinRing.Algebra.type Equality.type FinRing.Algebra.type. +check_join FinRing.Algebra.type FinGroup.type FinRing.Algebra.type. +check_join FinRing.Algebra.type FinRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Algebra.type FinRing.Lalgebra.type FinRing.Algebra.type. +check_join FinRing.Algebra.type FinRing.Lmodule.type FinRing.Algebra.type. +check_join FinRing.Algebra.type FinRing.Ring.type FinRing.Algebra.type. +check_join FinRing.Algebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Algebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Algebra.type FinRing.Zmodule.type FinRing.Algebra.type. +check_join FinRing.Algebra.type Finite.type FinRing.Algebra.type. +check_join FinRing.Algebra.type GRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Algebra.type GRing.Lalgebra.type FinRing.Algebra.type. +check_join FinRing.Algebra.type GRing.Lmodule.type FinRing.Algebra.type. +check_join FinRing.Algebra.type GRing.Ring.type FinRing.Algebra.type. +check_join FinRing.Algebra.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Algebra.type GRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Algebra.type GRing.Zmodule.type FinRing.Algebra.type. +check_join FinRing.ComRing.type Choice.type FinRing.ComRing.type. +check_join FinRing.ComRing.type CountRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.ComRing.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComRing.type CountRing.Field.type FinRing.Field.type. +check_join FinRing.ComRing.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.ComRing.type CountRing.Ring.type FinRing.ComRing.type. +check_join FinRing.ComRing.type CountRing.UnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComRing.type CountRing.Zmodule.type FinRing.ComRing.type. +check_join FinRing.ComRing.type Countable.type FinRing.ComRing.type. +check_join FinRing.ComRing.type Equality.type FinRing.ComRing.type. +check_join FinRing.ComRing.type FinGroup.type FinRing.ComRing.type. +check_join FinRing.ComRing.type FinRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.ComRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComRing.type FinRing.Field.type FinRing.Field.type. +check_join FinRing.ComRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.ComRing.type FinRing.Ring.type FinRing.ComRing.type. +check_join FinRing.ComRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComRing.type FinRing.Zmodule.type FinRing.ComRing.type. +check_join FinRing.ComRing.type Finite.type FinRing.ComRing.type. +check_join FinRing.ComRing.type GRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.ComRing.type GRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComRing.type GRing.Field.type FinRing.Field.type. +check_join FinRing.ComRing.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.ComRing.type GRing.Ring.type FinRing.ComRing.type. +check_join FinRing.ComRing.type GRing.UnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComRing.type GRing.Zmodule.type FinRing.ComRing.type. +check_join FinRing.ComUnitRing.type Choice.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type CountRing.ComRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type CountRing.Field.type FinRing.Field.type. +check_join FinRing.ComUnitRing.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.ComUnitRing.type CountRing.Ring.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type CountRing.UnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type CountRing.Zmodule.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type Countable.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type Equality.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type FinGroup.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type FinRing.Field.type FinRing.Field.type. +check_join FinRing.ComUnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.ComUnitRing.type FinRing.Ring.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type FinRing.Zmodule.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type Finite.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type GRing.ComRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type GRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type GRing.Field.type FinRing.Field.type. +check_join FinRing.ComUnitRing.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.ComUnitRing.type GRing.Ring.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type GRing.UnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.ComUnitRing.type GRing.Zmodule.type FinRing.ComUnitRing.type. +check_join FinRing.Field.type Choice.type FinRing.Field.type. +check_join FinRing.Field.type CountRing.ComRing.type FinRing.Field.type. +check_join FinRing.Field.type CountRing.ComUnitRing.type FinRing.Field.type. +check_join FinRing.Field.type CountRing.Field.type FinRing.Field.type. +check_join FinRing.Field.type CountRing.IntegralDomain.type FinRing.Field.type. +check_join FinRing.Field.type CountRing.Ring.type FinRing.Field.type. +check_join FinRing.Field.type CountRing.UnitRing.type FinRing.Field.type. +check_join FinRing.Field.type CountRing.Zmodule.type FinRing.Field.type. +check_join FinRing.Field.type Countable.type FinRing.Field.type. +check_join FinRing.Field.type Equality.type FinRing.Field.type. +check_join FinRing.Field.type FinGroup.type FinRing.Field.type. +check_join FinRing.Field.type FinRing.ComRing.type FinRing.Field.type. +check_join FinRing.Field.type FinRing.ComUnitRing.type FinRing.Field.type. +check_join FinRing.Field.type FinRing.Field.type FinRing.Field.type. +check_join FinRing.Field.type FinRing.IntegralDomain.type FinRing.Field.type. +check_join FinRing.Field.type FinRing.Ring.type FinRing.Field.type. +check_join FinRing.Field.type FinRing.UnitRing.type FinRing.Field.type. +check_join FinRing.Field.type FinRing.Zmodule.type FinRing.Field.type. +check_join FinRing.Field.type Finite.type FinRing.Field.type. +check_join FinRing.Field.type GRing.ComRing.type FinRing.Field.type. +check_join FinRing.Field.type GRing.ComUnitRing.type FinRing.Field.type. +check_join FinRing.Field.type GRing.Field.type FinRing.Field.type. +check_join FinRing.Field.type GRing.IntegralDomain.type FinRing.Field.type. +check_join FinRing.Field.type GRing.Ring.type FinRing.Field.type. +check_join FinRing.Field.type GRing.UnitRing.type FinRing.Field.type. +check_join FinRing.Field.type GRing.Zmodule.type FinRing.Field.type. +check_join FinRing.IntegralDomain.type Choice.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type CountRing.ComRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type CountRing.ComUnitRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type CountRing.Field.type FinRing.Field.type. +check_join FinRing.IntegralDomain.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type CountRing.Ring.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type CountRing.UnitRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type CountRing.Zmodule.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type Countable.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type Equality.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type FinGroup.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type FinRing.ComRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type FinRing.ComUnitRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type FinRing.Field.type FinRing.Field.type. +check_join FinRing.IntegralDomain.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type FinRing.Ring.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type FinRing.UnitRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type FinRing.Zmodule.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type Finite.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type GRing.ComRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type GRing.ComUnitRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type GRing.Field.type FinRing.Field.type. +check_join FinRing.IntegralDomain.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type GRing.Ring.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type GRing.UnitRing.type FinRing.IntegralDomain.type. +check_join FinRing.IntegralDomain.type GRing.Zmodule.type FinRing.IntegralDomain.type. +check_join FinRing.Lalgebra.type Choice.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type CountRing.Ring.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Lalgebra.type CountRing.Zmodule.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type Countable.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type Equality.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type FinGroup.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type FinRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Lalgebra.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type FinRing.Lmodule.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type FinRing.Ring.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Lalgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Lalgebra.type FinRing.Zmodule.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type Finite.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type GRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Lalgebra.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type GRing.Lmodule.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type GRing.Ring.type FinRing.Lalgebra.type. +check_join FinRing.Lalgebra.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Lalgebra.type GRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Lalgebra.type GRing.Zmodule.type FinRing.Lalgebra.type. +check_join FinRing.Lmodule.type Choice.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type CountRing.Ring.type FinRing.Lalgebra.type. +check_join FinRing.Lmodule.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Lmodule.type CountRing.Zmodule.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type Countable.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type Equality.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type FinGroup.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type FinRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Lmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Lmodule.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type FinRing.Ring.type FinRing.Lalgebra.type. +check_join FinRing.Lmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Lmodule.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Lmodule.type FinRing.Zmodule.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type Finite.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type GRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Lmodule.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Lmodule.type GRing.Lmodule.type FinRing.Lmodule.type. +check_join FinRing.Lmodule.type GRing.Ring.type FinRing.Lalgebra.type. +check_join FinRing.Lmodule.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Lmodule.type GRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.Lmodule.type GRing.Zmodule.type FinRing.Lmodule.type. +check_join FinRing.Ring.type Choice.type FinRing.Ring.type. +check_join FinRing.Ring.type CountRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.Ring.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.Ring.type CountRing.Field.type FinRing.Field.type. +check_join FinRing.Ring.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.Ring.type CountRing.Ring.type FinRing.Ring.type. +check_join FinRing.Ring.type CountRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.Ring.type CountRing.Zmodule.type FinRing.Ring.type. +check_join FinRing.Ring.type Countable.type FinRing.Ring.type. +check_join FinRing.Ring.type Equality.type FinRing.Ring.type. +check_join FinRing.Ring.type FinGroup.type FinRing.Ring.type. +check_join FinRing.Ring.type FinRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Ring.type FinRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.Ring.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.Ring.type FinRing.Field.type FinRing.Field.type. +check_join FinRing.Ring.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.Ring.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Ring.type FinRing.Lmodule.type FinRing.Lalgebra.type. +check_join FinRing.Ring.type FinRing.Ring.type FinRing.Ring.type. +check_join FinRing.Ring.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Ring.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.Ring.type FinRing.Zmodule.type FinRing.Ring.type. +check_join FinRing.Ring.type Finite.type FinRing.Ring.type. +check_join FinRing.Ring.type GRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Ring.type GRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.Ring.type GRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.Ring.type GRing.Field.type FinRing.Field.type. +check_join FinRing.Ring.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.Ring.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Ring.type GRing.Lmodule.type FinRing.Lalgebra.type. +check_join FinRing.Ring.type GRing.Ring.type FinRing.Ring.type. +check_join FinRing.Ring.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Ring.type GRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.Ring.type GRing.Zmodule.type FinRing.Ring.type. +check_join FinRing.UnitAlgebra.type Choice.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type CountRing.Ring.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type CountRing.Zmodule.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type Countable.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type Equality.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinGroup.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinRing.Algebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinRing.Ring.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type FinRing.Zmodule.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type Finite.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type GRing.Algebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type GRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type GRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type GRing.Ring.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type GRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitAlgebra.type GRing.Zmodule.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type Choice.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type CountRing.ComRing.type FinRing.ComUnitRing.type. +check_join FinRing.UnitRing.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.UnitRing.type CountRing.Field.type FinRing.Field.type. +check_join FinRing.UnitRing.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.UnitRing.type CountRing.Ring.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type CountRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type CountRing.Zmodule.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type Countable.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type Equality.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type FinGroup.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type FinRing.Algebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type. +check_join FinRing.UnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.UnitRing.type FinRing.Field.type FinRing.Field.type. +check_join FinRing.UnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.UnitRing.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type FinRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type FinRing.Ring.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type FinRing.Zmodule.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type Finite.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type GRing.Algebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type GRing.ComRing.type FinRing.ComUnitRing.type. +check_join FinRing.UnitRing.type GRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.UnitRing.type GRing.Field.type FinRing.Field.type. +check_join FinRing.UnitRing.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.UnitRing.type GRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type GRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type GRing.Ring.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.UnitRing.type GRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.UnitRing.type GRing.Zmodule.type FinRing.UnitRing.type. +check_join FinRing.Zmodule.type Choice.type FinRing.Zmodule.type. +check_join FinRing.Zmodule.type CountRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.Zmodule.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.Zmodule.type CountRing.Field.type FinRing.Field.type. +check_join FinRing.Zmodule.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.Zmodule.type CountRing.Ring.type FinRing.Ring.type. +check_join FinRing.Zmodule.type CountRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.Zmodule.type CountRing.Zmodule.type FinRing.Zmodule.type. +check_join FinRing.Zmodule.type Countable.type FinRing.Zmodule.type. +check_join FinRing.Zmodule.type Equality.type FinRing.Zmodule.type. +check_join FinRing.Zmodule.type FinGroup.type FinRing.Zmodule.type. +check_join FinRing.Zmodule.type FinRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Zmodule.type FinRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.Zmodule.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.Zmodule.type FinRing.Field.type FinRing.Field.type. +check_join FinRing.Zmodule.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.Zmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Zmodule.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join FinRing.Zmodule.type FinRing.Ring.type FinRing.Ring.type. +check_join FinRing.Zmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Zmodule.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.Zmodule.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join FinRing.Zmodule.type Finite.type FinRing.Zmodule.type. +check_join FinRing.Zmodule.type GRing.Algebra.type FinRing.Algebra.type. +check_join FinRing.Zmodule.type GRing.ComRing.type FinRing.ComRing.type. +check_join FinRing.Zmodule.type GRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join FinRing.Zmodule.type GRing.Field.type FinRing.Field.type. +check_join FinRing.Zmodule.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join FinRing.Zmodule.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join FinRing.Zmodule.type GRing.Lmodule.type FinRing.Lmodule.type. +check_join FinRing.Zmodule.type GRing.Ring.type FinRing.Ring.type. +check_join FinRing.Zmodule.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join FinRing.Zmodule.type GRing.UnitRing.type FinRing.UnitRing.type. +check_join FinRing.Zmodule.type GRing.Zmodule.type FinRing.Zmodule.type. +check_join Finite.type Choice.type Finite.type. +check_join Finite.type CountRing.ComRing.type FinRing.ComRing.type. +check_join Finite.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join Finite.type CountRing.Field.type FinRing.Field.type. +check_join Finite.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join Finite.type CountRing.Ring.type FinRing.Ring.type. +check_join Finite.type CountRing.UnitRing.type FinRing.UnitRing.type. +check_join Finite.type CountRing.Zmodule.type FinRing.Zmodule.type. +check_join Finite.type Countable.type Finite.type. +check_join Finite.type Equality.type Finite.type. +check_join Finite.type FinGroup.type FinGroup.type. +check_join Finite.type FinRing.Algebra.type FinRing.Algebra.type. +check_join Finite.type FinRing.ComRing.type FinRing.ComRing.type. +check_join Finite.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join Finite.type FinRing.Field.type FinRing.Field.type. +check_join Finite.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join Finite.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join Finite.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join Finite.type FinRing.Ring.type FinRing.Ring.type. +check_join Finite.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join Finite.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join Finite.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join Finite.type Finite.type Finite.type. +check_join Finite.type GRing.Algebra.type FinRing.Algebra.type. +check_join Finite.type GRing.ComRing.type FinRing.ComRing.type. +check_join Finite.type GRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join Finite.type GRing.Field.type FinRing.Field.type. +check_join Finite.type GRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join Finite.type GRing.Lalgebra.type FinRing.Lalgebra.type. +check_join Finite.type GRing.Lmodule.type FinRing.Lmodule.type. +check_join Finite.type GRing.Ring.type FinRing.Ring.type. +check_join Finite.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join Finite.type GRing.UnitRing.type FinRing.UnitRing.type. +check_join Finite.type GRing.Zmodule.type FinRing.Zmodule.type. +check_join GRing.Algebra.type Choice.type GRing.Algebra.type. +check_join GRing.Algebra.type CountRing.Ring.type FinRing.Algebra.type. +check_join GRing.Algebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.Algebra.type CountRing.Zmodule.type FinRing.Algebra.type. +check_join GRing.Algebra.type Countable.type FinRing.Algebra.type. +check_join GRing.Algebra.type Equality.type GRing.Algebra.type. +check_join GRing.Algebra.type Falgebra.type Falgebra.type. +check_join GRing.Algebra.type FieldExt.type FieldExt.type. +check_join GRing.Algebra.type FinGroup.type FinRing.Algebra.type. +check_join GRing.Algebra.type FinRing.Algebra.type FinRing.Algebra.type. +check_join GRing.Algebra.type FinRing.Lalgebra.type FinRing.Algebra.type. +check_join GRing.Algebra.type FinRing.Lmodule.type FinRing.Algebra.type. +check_join GRing.Algebra.type FinRing.Ring.type FinRing.Algebra.type. +check_join GRing.Algebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join GRing.Algebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.Algebra.type FinRing.Zmodule.type FinRing.Algebra.type. +check_join GRing.Algebra.type Finite.type FinRing.Algebra.type. +check_join GRing.Algebra.type GRing.Algebra.type GRing.Algebra.type. +check_join GRing.Algebra.type GRing.ComRing.type FieldExt.type. +check_join GRing.Algebra.type GRing.ComUnitRing.type FieldExt.type. +check_join GRing.Algebra.type GRing.Field.type FieldExt.type. +check_join GRing.Algebra.type GRing.IntegralDomain.type FieldExt.type. +check_join GRing.Algebra.type GRing.Lalgebra.type GRing.Algebra.type. +check_join GRing.Algebra.type GRing.Lmodule.type GRing.Algebra.type. +check_join GRing.Algebra.type GRing.Ring.type GRing.Algebra.type. +check_join GRing.Algebra.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join GRing.Algebra.type GRing.UnitRing.type GRing.UnitAlgebra.type. +check_join GRing.Algebra.type GRing.Zmodule.type GRing.Algebra.type. +check_join GRing.Algebra.type SplittingField.type SplittingField.type. +check_join GRing.Algebra.type Vector.type Falgebra.type. +check_join GRing.ClosedField.type Choice.type GRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.ComRing.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.ComUnitRing.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.DecidableField.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.Field.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.IntegralDomain.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.Ring.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.UnitRing.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type CountRing.Zmodule.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type Countable.type CountRing.ClosedField.type. +check_join GRing.ClosedField.type Equality.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.ComRing.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.ComUnitRing.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.DecidableField.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.Field.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.IntegralDomain.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.Ring.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.UnitRing.type GRing.ClosedField.type. +check_join GRing.ClosedField.type GRing.Zmodule.type GRing.ClosedField.type. +check_join GRing.ClosedField.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.ClosedField.type Num.NumDomain.type Num.ClosedField.type. +check_join GRing.ClosedField.type Num.NumField.type Num.ClosedField.type. +check_join GRing.ComRing.type Choice.type GRing.ComRing.type. +check_join GRing.ComRing.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.ComRing.type CountRing.ComRing.type CountRing.ComRing.type. +check_join GRing.ComRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join GRing.ComRing.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.ComRing.type CountRing.Field.type CountRing.Field.type. +check_join GRing.ComRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join GRing.ComRing.type CountRing.Ring.type CountRing.ComRing.type. +check_join GRing.ComRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type. +check_join GRing.ComRing.type CountRing.Zmodule.type CountRing.ComRing.type. +check_join GRing.ComRing.type Countable.type CountRing.ComRing.type. +check_join GRing.ComRing.type Equality.type GRing.ComRing.type. +check_join GRing.ComRing.type Falgebra.type FieldExt.type. +check_join GRing.ComRing.type FieldExt.type FieldExt.type. +check_join GRing.ComRing.type FinGroup.type FinRing.ComRing.type. +check_join GRing.ComRing.type FinRing.ComRing.type FinRing.ComRing.type. +check_join GRing.ComRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join GRing.ComRing.type FinRing.Field.type FinRing.Field.type. +check_join GRing.ComRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join GRing.ComRing.type FinRing.Ring.type FinRing.ComRing.type. +check_join GRing.ComRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type. +check_join GRing.ComRing.type FinRing.Zmodule.type FinRing.ComRing.type. +check_join GRing.ComRing.type Finite.type FinRing.ComRing.type. +check_join GRing.ComRing.type GRing.Algebra.type FieldExt.type. +check_join GRing.ComRing.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.ComRing.type GRing.ComRing.type GRing.ComRing.type. +check_join GRing.ComRing.type GRing.ComUnitRing.type GRing.ComUnitRing.type. +check_join GRing.ComRing.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.ComRing.type GRing.Field.type GRing.Field.type. +check_join GRing.ComRing.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join GRing.ComRing.type GRing.Lalgebra.type FieldExt.type. +check_join GRing.ComRing.type GRing.Lmodule.type FieldExt.type. +check_join GRing.ComRing.type GRing.Ring.type GRing.ComRing.type. +check_join GRing.ComRing.type GRing.UnitAlgebra.type FieldExt.type. +check_join GRing.ComRing.type GRing.UnitRing.type GRing.ComUnitRing.type. +check_join GRing.ComRing.type GRing.Zmodule.type GRing.ComRing.type. +check_join GRing.ComRing.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join GRing.ComRing.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.ComRing.type Num.NumDomain.type Num.NumDomain.type. +check_join GRing.ComRing.type Num.NumField.type Num.NumField.type. +check_join GRing.ComRing.type Num.RealClosedField.type Num.RealClosedField.type. +check_join GRing.ComRing.type Num.RealDomain.type Num.RealDomain.type. +check_join GRing.ComRing.type Num.RealField.type Num.RealField.type. +check_join GRing.ComRing.type SplittingField.type SplittingField.type. +check_join GRing.ComRing.type Vector.type FieldExt.type. +check_join GRing.ComUnitRing.type Choice.type GRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.ComUnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.ComUnitRing.type CountRing.Field.type CountRing.Field.type. +check_join GRing.ComUnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join GRing.ComUnitRing.type CountRing.Ring.type CountRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type CountRing.Zmodule.type CountRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type Countable.type CountRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type Equality.type GRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type Falgebra.type FieldExt.type. +check_join GRing.ComUnitRing.type FieldExt.type FieldExt.type. +check_join GRing.ComUnitRing.type FinGroup.type FinRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type FinRing.Field.type FinRing.Field.type. +check_join GRing.ComUnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join GRing.ComUnitRing.type FinRing.Ring.type FinRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type FinRing.Zmodule.type FinRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type Finite.type FinRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type GRing.Algebra.type FieldExt.type. +check_join GRing.ComUnitRing.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.ComUnitRing.type GRing.ComRing.type GRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type GRing.ComUnitRing.type GRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.ComUnitRing.type GRing.Field.type GRing.Field.type. +check_join GRing.ComUnitRing.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join GRing.ComUnitRing.type GRing.Lalgebra.type FieldExt.type. +check_join GRing.ComUnitRing.type GRing.Lmodule.type FieldExt.type. +check_join GRing.ComUnitRing.type GRing.Ring.type GRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type GRing.UnitAlgebra.type FieldExt.type. +check_join GRing.ComUnitRing.type GRing.UnitRing.type GRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type GRing.Zmodule.type GRing.ComUnitRing.type. +check_join GRing.ComUnitRing.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join GRing.ComUnitRing.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.ComUnitRing.type Num.NumDomain.type Num.NumDomain.type. +check_join GRing.ComUnitRing.type Num.NumField.type Num.NumField.type. +check_join GRing.ComUnitRing.type Num.RealClosedField.type Num.RealClosedField.type. +check_join GRing.ComUnitRing.type Num.RealDomain.type Num.RealDomain.type. +check_join GRing.ComUnitRing.type Num.RealField.type Num.RealField.type. +check_join GRing.ComUnitRing.type SplittingField.type SplittingField.type. +check_join GRing.ComUnitRing.type Vector.type FieldExt.type. +check_join GRing.DecidableField.type Choice.type GRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.DecidableField.type CountRing.ComRing.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.ComUnitRing.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.Field.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.IntegralDomain.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.Ring.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.UnitRing.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type CountRing.Zmodule.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type Countable.type CountRing.DecidableField.type. +check_join GRing.DecidableField.type Equality.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.DecidableField.type GRing.ComRing.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.ComUnitRing.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.Field.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.IntegralDomain.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.Ring.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.UnitRing.type GRing.DecidableField.type. +check_join GRing.DecidableField.type GRing.Zmodule.type GRing.DecidableField.type. +check_join GRing.DecidableField.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.DecidableField.type Num.NumDomain.type Num.ClosedField.type. +check_join GRing.DecidableField.type Num.NumField.type Num.ClosedField.type. +check_join GRing.Field.type Choice.type GRing.Field.type. +check_join GRing.Field.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.Field.type CountRing.ComRing.type CountRing.Field.type. +check_join GRing.Field.type CountRing.ComUnitRing.type CountRing.Field.type. +check_join GRing.Field.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.Field.type CountRing.Field.type CountRing.Field.type. +check_join GRing.Field.type CountRing.IntegralDomain.type CountRing.Field.type. +check_join GRing.Field.type CountRing.Ring.type CountRing.Field.type. +check_join GRing.Field.type CountRing.UnitRing.type CountRing.Field.type. +check_join GRing.Field.type CountRing.Zmodule.type CountRing.Field.type. +check_join GRing.Field.type Countable.type CountRing.Field.type. +check_join GRing.Field.type Equality.type GRing.Field.type. +check_join GRing.Field.type Falgebra.type FieldExt.type. +check_join GRing.Field.type FieldExt.type FieldExt.type. +check_join GRing.Field.type FinGroup.type FinRing.Field.type. +check_join GRing.Field.type FinRing.ComRing.type FinRing.Field.type. +check_join GRing.Field.type FinRing.ComUnitRing.type FinRing.Field.type. +check_join GRing.Field.type FinRing.Field.type FinRing.Field.type. +check_join GRing.Field.type FinRing.IntegralDomain.type FinRing.Field.type. +check_join GRing.Field.type FinRing.Ring.type FinRing.Field.type. +check_join GRing.Field.type FinRing.UnitRing.type FinRing.Field.type. +check_join GRing.Field.type FinRing.Zmodule.type FinRing.Field.type. +check_join GRing.Field.type Finite.type FinRing.Field.type. +check_join GRing.Field.type GRing.Algebra.type FieldExt.type. +check_join GRing.Field.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.Field.type GRing.ComRing.type GRing.Field.type. +check_join GRing.Field.type GRing.ComUnitRing.type GRing.Field.type. +check_join GRing.Field.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.Field.type GRing.Field.type GRing.Field.type. +check_join GRing.Field.type GRing.IntegralDomain.type GRing.Field.type. +check_join GRing.Field.type GRing.Lalgebra.type FieldExt.type. +check_join GRing.Field.type GRing.Lmodule.type FieldExt.type. +check_join GRing.Field.type GRing.Ring.type GRing.Field.type. +check_join GRing.Field.type GRing.UnitAlgebra.type FieldExt.type. +check_join GRing.Field.type GRing.UnitRing.type GRing.Field.type. +check_join GRing.Field.type GRing.Zmodule.type GRing.Field.type. +check_join GRing.Field.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join GRing.Field.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.Field.type Num.NumDomain.type Num.NumField.type. +check_join GRing.Field.type Num.NumField.type Num.NumField.type. +check_join GRing.Field.type Num.RealClosedField.type Num.RealClosedField.type. +check_join GRing.Field.type Num.RealDomain.type Num.RealField.type. +check_join GRing.Field.type Num.RealField.type Num.RealField.type. +check_join GRing.Field.type SplittingField.type SplittingField.type. +check_join GRing.Field.type Vector.type FieldExt.type. +check_join GRing.IntegralDomain.type Choice.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.IntegralDomain.type CountRing.ComRing.type CountRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type CountRing.ComUnitRing.type CountRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.IntegralDomain.type CountRing.Field.type CountRing.Field.type. +check_join GRing.IntegralDomain.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type CountRing.Ring.type CountRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type CountRing.UnitRing.type CountRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type CountRing.Zmodule.type CountRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type Countable.type CountRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type Equality.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type Falgebra.type FieldExt.type. +check_join GRing.IntegralDomain.type FieldExt.type FieldExt.type. +check_join GRing.IntegralDomain.type FinGroup.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type FinRing.ComRing.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type FinRing.ComUnitRing.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type FinRing.Field.type FinRing.Field.type. +check_join GRing.IntegralDomain.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type FinRing.Ring.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type FinRing.UnitRing.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type FinRing.Zmodule.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type Finite.type FinRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type GRing.Algebra.type FieldExt.type. +check_join GRing.IntegralDomain.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.IntegralDomain.type GRing.ComRing.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type GRing.ComUnitRing.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.IntegralDomain.type GRing.Field.type GRing.Field.type. +check_join GRing.IntegralDomain.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type GRing.Lalgebra.type FieldExt.type. +check_join GRing.IntegralDomain.type GRing.Lmodule.type FieldExt.type. +check_join GRing.IntegralDomain.type GRing.Ring.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type GRing.UnitAlgebra.type FieldExt.type. +check_join GRing.IntegralDomain.type GRing.UnitRing.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type GRing.Zmodule.type GRing.IntegralDomain.type. +check_join GRing.IntegralDomain.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join GRing.IntegralDomain.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.IntegralDomain.type Num.NumDomain.type Num.NumDomain.type. +check_join GRing.IntegralDomain.type Num.NumField.type Num.NumField.type. +check_join GRing.IntegralDomain.type Num.RealClosedField.type Num.RealClosedField.type. +check_join GRing.IntegralDomain.type Num.RealDomain.type Num.RealDomain.type. +check_join GRing.IntegralDomain.type Num.RealField.type Num.RealField.type. +check_join GRing.IntegralDomain.type SplittingField.type SplittingField.type. +check_join GRing.IntegralDomain.type Vector.type FieldExt.type. +check_join GRing.Lalgebra.type Choice.type GRing.Lalgebra.type. +check_join GRing.Lalgebra.type CountRing.Ring.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.Lalgebra.type CountRing.Zmodule.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type Countable.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type Equality.type GRing.Lalgebra.type. +check_join GRing.Lalgebra.type Falgebra.type Falgebra.type. +check_join GRing.Lalgebra.type FieldExt.type FieldExt.type. +check_join GRing.Lalgebra.type FinGroup.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type FinRing.Algebra.type FinRing.Algebra.type. +check_join GRing.Lalgebra.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type FinRing.Lmodule.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type FinRing.Ring.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join GRing.Lalgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.Lalgebra.type FinRing.Zmodule.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type Finite.type FinRing.Lalgebra.type. +check_join GRing.Lalgebra.type GRing.Algebra.type GRing.Algebra.type. +check_join GRing.Lalgebra.type GRing.ComRing.type FieldExt.type. +check_join GRing.Lalgebra.type GRing.ComUnitRing.type FieldExt.type. +check_join GRing.Lalgebra.type GRing.Field.type FieldExt.type. +check_join GRing.Lalgebra.type GRing.IntegralDomain.type FieldExt.type. +check_join GRing.Lalgebra.type GRing.Lalgebra.type GRing.Lalgebra.type. +check_join GRing.Lalgebra.type GRing.Lmodule.type GRing.Lalgebra.type. +check_join GRing.Lalgebra.type GRing.Ring.type GRing.Lalgebra.type. +check_join GRing.Lalgebra.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join GRing.Lalgebra.type GRing.UnitRing.type GRing.UnitAlgebra.type. +check_join GRing.Lalgebra.type GRing.Zmodule.type GRing.Lalgebra.type. +check_join GRing.Lalgebra.type SplittingField.type SplittingField.type. +check_join GRing.Lalgebra.type Vector.type Falgebra.type. +check_join GRing.Lmodule.type Choice.type GRing.Lmodule.type. +check_join GRing.Lmodule.type CountRing.Ring.type FinRing.Lalgebra.type. +check_join GRing.Lmodule.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.Lmodule.type CountRing.Zmodule.type FinRing.Lmodule.type. +check_join GRing.Lmodule.type Countable.type FinRing.Lmodule.type. +check_join GRing.Lmodule.type Equality.type GRing.Lmodule.type. +check_join GRing.Lmodule.type Falgebra.type Falgebra.type. +check_join GRing.Lmodule.type FieldExt.type FieldExt.type. +check_join GRing.Lmodule.type FinGroup.type FinRing.Lmodule.type. +check_join GRing.Lmodule.type FinRing.Algebra.type FinRing.Algebra.type. +check_join GRing.Lmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join GRing.Lmodule.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join GRing.Lmodule.type FinRing.Ring.type FinRing.Lalgebra.type. +check_join GRing.Lmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join GRing.Lmodule.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.Lmodule.type FinRing.Zmodule.type FinRing.Lmodule.type. +check_join GRing.Lmodule.type Finite.type FinRing.Lmodule.type. +check_join GRing.Lmodule.type GRing.Algebra.type GRing.Algebra.type. +check_join GRing.Lmodule.type GRing.ComRing.type FieldExt.type. +check_join GRing.Lmodule.type GRing.ComUnitRing.type FieldExt.type. +check_join GRing.Lmodule.type GRing.Field.type FieldExt.type. +check_join GRing.Lmodule.type GRing.IntegralDomain.type FieldExt.type. +check_join GRing.Lmodule.type GRing.Lalgebra.type GRing.Lalgebra.type. +check_join GRing.Lmodule.type GRing.Lmodule.type GRing.Lmodule.type. +check_join GRing.Lmodule.type GRing.Ring.type GRing.Lalgebra.type. +check_join GRing.Lmodule.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join GRing.Lmodule.type GRing.UnitRing.type GRing.UnitAlgebra.type. +check_join GRing.Lmodule.type GRing.Zmodule.type GRing.Lmodule.type. +check_join GRing.Lmodule.type SplittingField.type SplittingField.type. +check_join GRing.Lmodule.type Vector.type Vector.type. +check_join GRing.Ring.type Choice.type GRing.Ring.type. +check_join GRing.Ring.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.Ring.type CountRing.ComRing.type CountRing.ComRing.type. +check_join GRing.Ring.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join GRing.Ring.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.Ring.type CountRing.Field.type CountRing.Field.type. +check_join GRing.Ring.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join GRing.Ring.type CountRing.Ring.type CountRing.Ring.type. +check_join GRing.Ring.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join GRing.Ring.type CountRing.Zmodule.type CountRing.Ring.type. +check_join GRing.Ring.type Countable.type CountRing.Ring.type. +check_join GRing.Ring.type Equality.type GRing.Ring.type. +check_join GRing.Ring.type Falgebra.type Falgebra.type. +check_join GRing.Ring.type FieldExt.type FieldExt.type. +check_join GRing.Ring.type FinGroup.type FinRing.Ring.type. +check_join GRing.Ring.type FinRing.Algebra.type FinRing.Algebra.type. +check_join GRing.Ring.type FinRing.ComRing.type FinRing.ComRing.type. +check_join GRing.Ring.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join GRing.Ring.type FinRing.Field.type FinRing.Field.type. +check_join GRing.Ring.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join GRing.Ring.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join GRing.Ring.type FinRing.Lmodule.type FinRing.Lalgebra.type. +check_join GRing.Ring.type FinRing.Ring.type FinRing.Ring.type. +check_join GRing.Ring.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join GRing.Ring.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join GRing.Ring.type FinRing.Zmodule.type FinRing.Ring.type. +check_join GRing.Ring.type Finite.type FinRing.Ring.type. +check_join GRing.Ring.type GRing.Algebra.type GRing.Algebra.type. +check_join GRing.Ring.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.Ring.type GRing.ComRing.type GRing.ComRing.type. +check_join GRing.Ring.type GRing.ComUnitRing.type GRing.ComUnitRing.type. +check_join GRing.Ring.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.Ring.type GRing.Field.type GRing.Field.type. +check_join GRing.Ring.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join GRing.Ring.type GRing.Lalgebra.type GRing.Lalgebra.type. +check_join GRing.Ring.type GRing.Lmodule.type GRing.Lalgebra.type. +check_join GRing.Ring.type GRing.Ring.type GRing.Ring.type. +check_join GRing.Ring.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join GRing.Ring.type GRing.UnitRing.type GRing.UnitRing.type. +check_join GRing.Ring.type GRing.Zmodule.type GRing.Ring.type. +check_join GRing.Ring.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join GRing.Ring.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.Ring.type Num.NumDomain.type Num.NumDomain.type. +check_join GRing.Ring.type Num.NumField.type Num.NumField.type. +check_join GRing.Ring.type Num.RealClosedField.type Num.RealClosedField.type. +check_join GRing.Ring.type Num.RealDomain.type Num.RealDomain.type. +check_join GRing.Ring.type Num.RealField.type Num.RealField.type. +check_join GRing.Ring.type SplittingField.type SplittingField.type. +check_join GRing.Ring.type Vector.type Falgebra.type. +check_join GRing.UnitAlgebra.type Choice.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type CountRing.Ring.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type CountRing.Zmodule.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type Countable.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type Equality.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type Falgebra.type Falgebra.type. +check_join GRing.UnitAlgebra.type FieldExt.type FieldExt.type. +check_join GRing.UnitAlgebra.type FinGroup.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type FinRing.Algebra.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type FinRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type FinRing.Ring.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type FinRing.Zmodule.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type Finite.type FinRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type GRing.Algebra.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type GRing.ComRing.type FieldExt.type. +check_join GRing.UnitAlgebra.type GRing.ComUnitRing.type FieldExt.type. +check_join GRing.UnitAlgebra.type GRing.Field.type FieldExt.type. +check_join GRing.UnitAlgebra.type GRing.IntegralDomain.type FieldExt.type. +check_join GRing.UnitAlgebra.type GRing.Lalgebra.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type GRing.Lmodule.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type GRing.Ring.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type GRing.UnitRing.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type GRing.Zmodule.type GRing.UnitAlgebra.type. +check_join GRing.UnitAlgebra.type SplittingField.type SplittingField.type. +check_join GRing.UnitAlgebra.type Vector.type Falgebra.type. +check_join GRing.UnitRing.type Choice.type GRing.UnitRing.type. +check_join GRing.UnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.UnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type. +check_join GRing.UnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join GRing.UnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.UnitRing.type CountRing.Field.type CountRing.Field.type. +check_join GRing.UnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join GRing.UnitRing.type CountRing.Ring.type CountRing.UnitRing.type. +check_join GRing.UnitRing.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join GRing.UnitRing.type CountRing.Zmodule.type CountRing.UnitRing.type. +check_join GRing.UnitRing.type Countable.type CountRing.UnitRing.type. +check_join GRing.UnitRing.type Equality.type GRing.UnitRing.type. +check_join GRing.UnitRing.type Falgebra.type Falgebra.type. +check_join GRing.UnitRing.type FieldExt.type FieldExt.type. +check_join GRing.UnitRing.type FinGroup.type FinRing.UnitRing.type. +check_join GRing.UnitRing.type FinRing.Algebra.type FinRing.UnitAlgebra.type. +check_join GRing.UnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type. +check_join GRing.UnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join GRing.UnitRing.type FinRing.Field.type FinRing.Field.type. +check_join GRing.UnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join GRing.UnitRing.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type. +check_join GRing.UnitRing.type FinRing.Lmodule.type FinRing.UnitAlgebra.type. +check_join GRing.UnitRing.type FinRing.Ring.type FinRing.UnitRing.type. +check_join GRing.UnitRing.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join GRing.UnitRing.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join GRing.UnitRing.type FinRing.Zmodule.type FinRing.UnitRing.type. +check_join GRing.UnitRing.type Finite.type FinRing.UnitRing.type. +check_join GRing.UnitRing.type GRing.Algebra.type GRing.UnitAlgebra.type. +check_join GRing.UnitRing.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.UnitRing.type GRing.ComRing.type GRing.ComUnitRing.type. +check_join GRing.UnitRing.type GRing.ComUnitRing.type GRing.ComUnitRing.type. +check_join GRing.UnitRing.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.UnitRing.type GRing.Field.type GRing.Field.type. +check_join GRing.UnitRing.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join GRing.UnitRing.type GRing.Lalgebra.type GRing.UnitAlgebra.type. +check_join GRing.UnitRing.type GRing.Lmodule.type GRing.UnitAlgebra.type. +check_join GRing.UnitRing.type GRing.Ring.type GRing.UnitRing.type. +check_join GRing.UnitRing.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join GRing.UnitRing.type GRing.UnitRing.type GRing.UnitRing.type. +check_join GRing.UnitRing.type GRing.Zmodule.type GRing.UnitRing.type. +check_join GRing.UnitRing.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join GRing.UnitRing.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.UnitRing.type Num.NumDomain.type Num.NumDomain.type. +check_join GRing.UnitRing.type Num.NumField.type Num.NumField.type. +check_join GRing.UnitRing.type Num.RealClosedField.type Num.RealClosedField.type. +check_join GRing.UnitRing.type Num.RealDomain.type Num.RealDomain.type. +check_join GRing.UnitRing.type Num.RealField.type Num.RealField.type. +check_join GRing.UnitRing.type SplittingField.type SplittingField.type. +check_join GRing.UnitRing.type Vector.type Falgebra.type. +check_join GRing.Zmodule.type Choice.type GRing.Zmodule.type. +check_join GRing.Zmodule.type CountRing.ClosedField.type CountRing.ClosedField.type. +check_join GRing.Zmodule.type CountRing.ComRing.type CountRing.ComRing.type. +check_join GRing.Zmodule.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type. +check_join GRing.Zmodule.type CountRing.DecidableField.type CountRing.DecidableField.type. +check_join GRing.Zmodule.type CountRing.Field.type CountRing.Field.type. +check_join GRing.Zmodule.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type. +check_join GRing.Zmodule.type CountRing.Ring.type CountRing.Ring.type. +check_join GRing.Zmodule.type CountRing.UnitRing.type CountRing.UnitRing.type. +check_join GRing.Zmodule.type CountRing.Zmodule.type CountRing.Zmodule.type. +check_join GRing.Zmodule.type Countable.type CountRing.Zmodule.type. +check_join GRing.Zmodule.type Equality.type GRing.Zmodule.type. +check_join GRing.Zmodule.type Falgebra.type Falgebra.type. +check_join GRing.Zmodule.type FieldExt.type FieldExt.type. +check_join GRing.Zmodule.type FinGroup.type FinRing.Zmodule.type. +check_join GRing.Zmodule.type FinRing.Algebra.type FinRing.Algebra.type. +check_join GRing.Zmodule.type FinRing.ComRing.type FinRing.ComRing.type. +check_join GRing.Zmodule.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type. +check_join GRing.Zmodule.type FinRing.Field.type FinRing.Field.type. +check_join GRing.Zmodule.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type. +check_join GRing.Zmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type. +check_join GRing.Zmodule.type FinRing.Lmodule.type FinRing.Lmodule.type. +check_join GRing.Zmodule.type FinRing.Ring.type FinRing.Ring.type. +check_join GRing.Zmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type. +check_join GRing.Zmodule.type FinRing.UnitRing.type FinRing.UnitRing.type. +check_join GRing.Zmodule.type FinRing.Zmodule.type FinRing.Zmodule.type. +check_join GRing.Zmodule.type Finite.type FinRing.Zmodule.type. +check_join GRing.Zmodule.type GRing.Algebra.type GRing.Algebra.type. +check_join GRing.Zmodule.type GRing.ClosedField.type GRing.ClosedField.type. +check_join GRing.Zmodule.type GRing.ComRing.type GRing.ComRing.type. +check_join GRing.Zmodule.type GRing.ComUnitRing.type GRing.ComUnitRing.type. +check_join GRing.Zmodule.type GRing.DecidableField.type GRing.DecidableField.type. +check_join GRing.Zmodule.type GRing.Field.type GRing.Field.type. +check_join GRing.Zmodule.type GRing.IntegralDomain.type GRing.IntegralDomain.type. +check_join GRing.Zmodule.type GRing.Lalgebra.type GRing.Lalgebra.type. +check_join GRing.Zmodule.type GRing.Lmodule.type GRing.Lmodule.type. +check_join GRing.Zmodule.type GRing.Ring.type GRing.Ring.type. +check_join GRing.Zmodule.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type. +check_join GRing.Zmodule.type GRing.UnitRing.type GRing.UnitRing.type. +check_join GRing.Zmodule.type GRing.Zmodule.type GRing.Zmodule.type. +check_join GRing.Zmodule.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join GRing.Zmodule.type Num.ClosedField.type Num.ClosedField.type. +check_join GRing.Zmodule.type Num.NumDomain.type Num.NumDomain.type. +check_join GRing.Zmodule.type Num.NumField.type Num.NumField.type. +check_join GRing.Zmodule.type Num.RealClosedField.type Num.RealClosedField.type. +check_join GRing.Zmodule.type Num.RealDomain.type Num.RealDomain.type. +check_join GRing.Zmodule.type Num.RealField.type Num.RealField.type. +check_join GRing.Zmodule.type SplittingField.type SplittingField.type. +check_join GRing.Zmodule.type Vector.type Vector.type. +check_join Num.ArchimedeanField.type Choice.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type Equality.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type GRing.ComRing.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type GRing.ComUnitRing.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type GRing.Field.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type GRing.IntegralDomain.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type GRing.Ring.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type GRing.UnitRing.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type GRing.Zmodule.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type Num.NumDomain.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type Num.NumField.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type Num.RealDomain.type Num.ArchimedeanField.type. +check_join Num.ArchimedeanField.type Num.RealField.type Num.ArchimedeanField.type. +check_join Num.ClosedField.type Choice.type Num.ClosedField.type. +check_join Num.ClosedField.type Equality.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.ClosedField.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.ComRing.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.ComUnitRing.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.DecidableField.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.Field.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.IntegralDomain.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.Ring.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.UnitRing.type Num.ClosedField.type. +check_join Num.ClosedField.type GRing.Zmodule.type Num.ClosedField.type. +check_join Num.ClosedField.type Num.ClosedField.type Num.ClosedField.type. +check_join Num.ClosedField.type Num.NumDomain.type Num.ClosedField.type. +check_join Num.ClosedField.type Num.NumField.type Num.ClosedField.type. +check_join Num.NumDomain.type Choice.type Num.NumDomain.type. +check_join Num.NumDomain.type Equality.type Num.NumDomain.type. +check_join Num.NumDomain.type GRing.ClosedField.type Num.ClosedField.type. +check_join Num.NumDomain.type GRing.ComRing.type Num.NumDomain.type. +check_join Num.NumDomain.type GRing.ComUnitRing.type Num.NumDomain.type. +check_join Num.NumDomain.type GRing.DecidableField.type Num.ClosedField.type. +check_join Num.NumDomain.type GRing.Field.type Num.NumField.type. +check_join Num.NumDomain.type GRing.IntegralDomain.type Num.NumDomain.type. +check_join Num.NumDomain.type GRing.Ring.type Num.NumDomain.type. +check_join Num.NumDomain.type GRing.UnitRing.type Num.NumDomain.type. +check_join Num.NumDomain.type GRing.Zmodule.type Num.NumDomain.type. +check_join Num.NumDomain.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join Num.NumDomain.type Num.ClosedField.type Num.ClosedField.type. +check_join Num.NumDomain.type Num.NumDomain.type Num.NumDomain.type. +check_join Num.NumDomain.type Num.NumField.type Num.NumField.type. +check_join Num.NumDomain.type Num.RealClosedField.type Num.RealClosedField.type. +check_join Num.NumDomain.type Num.RealDomain.type Num.RealDomain.type. +check_join Num.NumDomain.type Num.RealField.type Num.RealField.type. +check_join Num.NumField.type Choice.type Num.NumField.type. +check_join Num.NumField.type Equality.type Num.NumField.type. +check_join Num.NumField.type GRing.ClosedField.type Num.ClosedField.type. +check_join Num.NumField.type GRing.ComRing.type Num.NumField.type. +check_join Num.NumField.type GRing.ComUnitRing.type Num.NumField.type. +check_join Num.NumField.type GRing.DecidableField.type Num.ClosedField.type. +check_join Num.NumField.type GRing.Field.type Num.NumField.type. +check_join Num.NumField.type GRing.IntegralDomain.type Num.NumField.type. +check_join Num.NumField.type GRing.Ring.type Num.NumField.type. +check_join Num.NumField.type GRing.UnitRing.type Num.NumField.type. +check_join Num.NumField.type GRing.Zmodule.type Num.NumField.type. +check_join Num.NumField.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join Num.NumField.type Num.ClosedField.type Num.ClosedField.type. +check_join Num.NumField.type Num.NumDomain.type Num.NumField.type. +check_join Num.NumField.type Num.NumField.type Num.NumField.type. +check_join Num.NumField.type Num.RealClosedField.type Num.RealClosedField.type. +check_join Num.NumField.type Num.RealDomain.type Num.RealField.type. +check_join Num.NumField.type Num.RealField.type Num.RealField.type. +check_join Num.RealClosedField.type Choice.type Num.RealClosedField.type. +check_join Num.RealClosedField.type Equality.type Num.RealClosedField.type. +check_join Num.RealClosedField.type GRing.ComRing.type Num.RealClosedField.type. +check_join Num.RealClosedField.type GRing.ComUnitRing.type Num.RealClosedField.type. +check_join Num.RealClosedField.type GRing.Field.type Num.RealClosedField.type. +check_join Num.RealClosedField.type GRing.IntegralDomain.type Num.RealClosedField.type. +check_join Num.RealClosedField.type GRing.Ring.type Num.RealClosedField.type. +check_join Num.RealClosedField.type GRing.UnitRing.type Num.RealClosedField.type. +check_join Num.RealClosedField.type GRing.Zmodule.type Num.RealClosedField.type. +check_join Num.RealClosedField.type Num.NumDomain.type Num.RealClosedField.type. +check_join Num.RealClosedField.type Num.NumField.type Num.RealClosedField.type. +check_join Num.RealClosedField.type Num.RealClosedField.type Num.RealClosedField.type. +check_join Num.RealClosedField.type Num.RealDomain.type Num.RealClosedField.type. +check_join Num.RealClosedField.type Num.RealField.type Num.RealClosedField.type. +check_join Num.RealDomain.type Choice.type Num.RealDomain.type. +check_join Num.RealDomain.type Equality.type Num.RealDomain.type. +check_join Num.RealDomain.type GRing.ComRing.type Num.RealDomain.type. +check_join Num.RealDomain.type GRing.ComUnitRing.type Num.RealDomain.type. +check_join Num.RealDomain.type GRing.Field.type Num.RealField.type. +check_join Num.RealDomain.type GRing.IntegralDomain.type Num.RealDomain.type. +check_join Num.RealDomain.type GRing.Ring.type Num.RealDomain.type. +check_join Num.RealDomain.type GRing.UnitRing.type Num.RealDomain.type. +check_join Num.RealDomain.type GRing.Zmodule.type Num.RealDomain.type. +check_join Num.RealDomain.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join Num.RealDomain.type Num.NumDomain.type Num.RealDomain.type. +check_join Num.RealDomain.type Num.NumField.type Num.RealField.type. +check_join Num.RealDomain.type Num.RealClosedField.type Num.RealClosedField.type. +check_join Num.RealDomain.type Num.RealDomain.type Num.RealDomain.type. +check_join Num.RealDomain.type Num.RealField.type Num.RealField.type. +check_join Num.RealField.type Choice.type Num.RealField.type. +check_join Num.RealField.type Equality.type Num.RealField.type. +check_join Num.RealField.type GRing.ComRing.type Num.RealField.type. +check_join Num.RealField.type GRing.ComUnitRing.type Num.RealField.type. +check_join Num.RealField.type GRing.Field.type Num.RealField.type. +check_join Num.RealField.type GRing.IntegralDomain.type Num.RealField.type. +check_join Num.RealField.type GRing.Ring.type Num.RealField.type. +check_join Num.RealField.type GRing.UnitRing.type Num.RealField.type. +check_join Num.RealField.type GRing.Zmodule.type Num.RealField.type. +check_join Num.RealField.type Num.ArchimedeanField.type Num.ArchimedeanField.type. +check_join Num.RealField.type Num.NumDomain.type Num.RealField.type. +check_join Num.RealField.type Num.NumField.type Num.RealField.type. +check_join Num.RealField.type Num.RealClosedField.type Num.RealClosedField.type. +check_join Num.RealField.type Num.RealDomain.type Num.RealField.type. +check_join Num.RealField.type Num.RealField.type Num.RealField.type. +check_join SplittingField.type Choice.type SplittingField.type. +check_join SplittingField.type Equality.type SplittingField.type. +check_join SplittingField.type Falgebra.type SplittingField.type. +check_join SplittingField.type FieldExt.type SplittingField.type. +check_join SplittingField.type GRing.Algebra.type SplittingField.type. +check_join SplittingField.type GRing.ComRing.type SplittingField.type. +check_join SplittingField.type GRing.ComUnitRing.type SplittingField.type. +check_join SplittingField.type GRing.Field.type SplittingField.type. +check_join SplittingField.type GRing.IntegralDomain.type SplittingField.type. +check_join SplittingField.type GRing.Lalgebra.type SplittingField.type. +check_join SplittingField.type GRing.Lmodule.type SplittingField.type. +check_join SplittingField.type GRing.Ring.type SplittingField.type. +check_join SplittingField.type GRing.UnitAlgebra.type SplittingField.type. +check_join SplittingField.type GRing.UnitRing.type SplittingField.type. +check_join SplittingField.type GRing.Zmodule.type SplittingField.type. +check_join SplittingField.type SplittingField.type SplittingField.type. +check_join SplittingField.type Vector.type SplittingField.type. +check_join Vector.type Choice.type Vector.type. +check_join Vector.type Equality.type Vector.type. +check_join Vector.type Falgebra.type Falgebra.type. +check_join Vector.type FieldExt.type FieldExt.type. +check_join Vector.type GRing.Algebra.type Falgebra.type. +check_join Vector.type GRing.ComRing.type FieldExt.type. +check_join Vector.type GRing.ComUnitRing.type FieldExt.type. +check_join Vector.type GRing.Field.type FieldExt.type. +check_join Vector.type GRing.IntegralDomain.type FieldExt.type. +check_join Vector.type GRing.Lalgebra.type Falgebra.type. +check_join Vector.type GRing.Lmodule.type Vector.type. +check_join Vector.type GRing.Ring.type Falgebra.type. +check_join Vector.type GRing.UnitAlgebra.type Falgebra.type. +check_join Vector.type GRing.UnitRing.type Falgebra.type. +check_join Vector.type GRing.Zmodule.type Vector.type. +check_join Vector.type SplittingField.type SplittingField.type. +check_join Vector.type Vector.type Vector.type. +Abort. |