Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/trace.class_instances.txt

Created September 20, 2018 18:00
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kbuzzard/2582db6593c7b7467f3e0020909af467 to your computer and use it in GitHub Desktop.
Save kbuzzard/2582db6593c7b7467f3e0020909af467 to your computer and use it in GitHub Desktop.
Download ZIP
trace.class_instances output
Raw
trace.class_instances.txt
scratch1.lean:7:9: information trace output
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_0 : has_add ↥S := @quotient_module.quotient.has_add ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ↥S := @is_submodule.has_add ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12
[class_instances] (1) ?x_9 : ring ?x_7 := _inst_1
[class_instances] (1) ?x_10 : @module ↥S R _inst_1 := @quotient_module.quotient.module ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18
failed is_def_eq
[class_instances] (1) ?x_10 : @module ↥S R _inst_1 := @is_submodule.module ?x_19 ?x_20 ?x_21 ?x_22 ?x_23 ?x_24
failed is_def_eq
[class_instances] (1) ?x_10 : @module ↥S R _inst_1 := @prod.module ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30
failed is_def_eq
[class_instances] (1) ?x_10 : @module ↥S R _inst_1 := @lc.module ?x_31 ?x_32 ?x_33 ?x_34
failed is_def_eq
[class_instances] (1) ?x_10 : @module ↥S R _inst_1 := @vector_space.to_module ?x_35 ?x_36 ?x_37 ?x_38
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_39 : field ↥S := @linear_ordered_field.to_field ?x_40 ?x_41
[class_instances] (1) ?x_41 : linear_ordered_field ↥S := @discrete_linear_ordered_field.to_linear_ordered_field ?x_42 ?x_43
[class_instances] (0) ?x_39 : field ↥S := @discrete_field.to_field ?x_40 ?x_41
[class_instances] (1) ?x_41 : discrete_field ↥S := @discrete_linear_ordered_field.to_discrete_field ?x_42 ?x_43
failed is_def_eq
[class_instances] (1) ?x_10 : @module ↥S R _inst_1 := @ring.to_module ?x_39 ?x_40
failed is_def_eq
[class_instances] (1) ?x_9 : ring ?x_7 := @prod.ring ?x_13 ?x_14 ?x_15 ?x_16
[class_instances] (2) ?x_15 : ring ?x_13 := _inst_1
[class_instances] (2) ?x_16 : ring ?x_14 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S) R (@prod.ring ↥S ↥S _inst_1 _inst_1) := @quotient_module.quotient.module ?x_17 ?x_18 ?x_19 ?x_20 ?x_21 ?x_22
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S) R (@prod.ring ↥S ↥S _inst_1 _inst_1) := @is_submodule.module ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S) R (@prod.ring ↥S ↥S _inst_1 _inst_1) := @prod.module ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S) R (@prod.ring ↥S ↥S _inst_1 _inst_1) := @lc.module ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S) R (@prod.ring ↥S ↥S _inst_1 _inst_1) := @vector_space.to_module ?x_39 ?x_40 ?x_41 ?x_42
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_43 : field (↥S × ↥S) := @linear_ordered_field.to_field ?x_44 ?x_45
[class_instances] (1) ?x_45 : linear_ordered_field (↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_46 ?x_47
[class_instances] (0) ?x_43 : field (↥S × ↥S) := @discrete_field.to_field ?x_44 ?x_45
[class_instances] (1) ?x_45 : discrete_field (↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_46 ?x_47
[class_instances] cached failure for field (↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S) R (@prod.ring ↥S ↥S _inst_1 _inst_1) := @ring.to_module ?x_43 ?x_44
failed is_def_eq
[class_instances] (2) ?x_16 : ring ?x_14 := @prod.ring ?x_17 ?x_18 ?x_19 ?x_20
[class_instances] (3) ?x_19 : ring ?x_17 := _inst_1
[class_instances] (3) ?x_20 : ring ?x_18 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S) R (@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)) := @quotient_module.quotient.module ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S) R (@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)) := @is_submodule.module ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S) R (@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)) := @prod.module ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S) R (@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)) := @lc.module ?x_39 ?x_40 ?x_41 ?x_42
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S) R (@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)) := @vector_space.to_module ?x_43 ?x_44 ?x_45 ?x_46
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_47 : field (↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_48 ?x_49
[class_instances] (1) ?x_49 : linear_ordered_field (↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_50 ?x_51
[class_instances] (0) ?x_47 : field (↥S × ↥S × ↥S) := @discrete_field.to_field ?x_48 ?x_49
[class_instances] (1) ?x_49 : discrete_field (↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_50 ?x_51
[class_instances] cached failure for field (↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S) R (@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)) := @ring.to_module ?x_47 ?x_48
failed is_def_eq
[class_instances] (3) ?x_20 : ring ?x_18 := @prod.ring ?x_21 ?x_22 ?x_23 ?x_24
[class_instances] (4) ?x_23 : ring ?x_21 := _inst_1
[class_instances] (4) ?x_24 : ring ?x_22 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))) := @quotient_module.quotient.module ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))) := @is_submodule.module ?x_31 ?x_32 ?x_33 ?x_34 ?x_35 ?x_36
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))) := @prod.module ?x_37 ?x_38 ?x_39 ?x_40 ?x_41 ?x_42
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))) := @lc.module ?x_43 ?x_44 ?x_45 ?x_46
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))) := @vector_space.to_module ?x_47 ?x_48 ?x_49 ?x_50
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_51 : field (↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_52 ?x_53
[class_instances] (1) ?x_53 : linear_ordered_field (↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_54 ?x_55
[class_instances] (0) ?x_51 : field (↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_52 ?x_53
[class_instances] (1) ?x_53 : discrete_field (↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_54 ?x_55
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))) := @ring.to_module ?x_51 ?x_52
failed is_def_eq
[class_instances] (4) ?x_24 : ring ?x_22 := @prod.ring ?x_25 ?x_26 ?x_27 ?x_28
[class_instances] (5) ?x_27 : ring ?x_25 := _inst_1
[class_instances] (5) ?x_28 : ring ?x_26 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))) := @quotient_module.quotient.module ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))) := @is_submodule.module ?x_35 ?x_36 ?x_37 ?x_38 ?x_39 ?x_40
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))) := @prod.module ?x_41 ?x_42 ?x_43 ?x_44 ?x_45 ?x_46
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))) := @lc.module ?x_47 ?x_48 ?x_49 ?x_50
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))) := @vector_space.to_module ?x_51 ?x_52 ?x_53 ?x_54
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_55 : field (↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_56 ?x_57
[class_instances] (1) ?x_57 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_58 ?x_59
[class_instances] (0) ?x_55 : field (↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_56 ?x_57
[class_instances] (1) ?x_57 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_58 ?x_59
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))) := @ring.to_module ?x_55 ?x_56
failed is_def_eq
[class_instances] (5) ?x_28 : ring ?x_26 := @prod.ring ?x_29 ?x_30 ?x_31 ?x_32
[class_instances] (6) ?x_31 : ring ?x_29 := _inst_1
[class_instances] (6) ?x_32 : ring ?x_30 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))) := @quotient_module.quotient.module ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))) := @is_submodule.module ?x_39 ?x_40 ?x_41 ?x_42 ?x_43 ?x_44
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))) := @prod.module ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 ?x_50
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))) := @lc.module ?x_51 ?x_52 ?x_53 ?x_54
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))) := @vector_space.to_module ?x_55 ?x_56 ?x_57 ?x_58
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_59 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_60 ?x_61
[class_instances] (1) ?x_61 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_62 ?x_63
[class_instances] (0) ?x_59 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_60 ?x_61
[class_instances] (1) ?x_61 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_62 ?x_63
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))) := @ring.to_module ?x_59 ?x_60
failed is_def_eq
[class_instances] (6) ?x_32 : ring ?x_30 := @prod.ring ?x_33 ?x_34 ?x_35 ?x_36
[class_instances] (7) ?x_35 : ring ?x_33 := _inst_1
[class_instances] (7) ?x_36 : ring ?x_34 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))) := @quotient_module.quotient.module ?x_37 ?x_38 ?x_39 ?x_40 ?x_41 ?x_42
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))) := @is_submodule.module ?x_43 ?x_44 ?x_45 ?x_46 ?x_47 ?x_48
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))) := @prod.module ?x_49 ?x_50 ?x_51 ?x_52 ?x_53 ?x_54
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))) := @lc.module ?x_55 ?x_56 ?x_57 ?x_58
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))) := @vector_space.to_module ?x_59 ?x_60 ?x_61 ?x_62
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_63 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_64 ?x_65
[class_instances] (1) ?x_65 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_66 ?x_67
[class_instances] (0) ?x_63 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_64 ?x_65
[class_instances] (1) ?x_65 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_66 ?x_67
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))) := @ring.to_module ?x_63 ?x_64
failed is_def_eq
[class_instances] (7) ?x_36 : ring ?x_34 := @prod.ring ?x_37 ?x_38 ?x_39 ?x_40
[class_instances] (8) ?x_39 : ring ?x_37 := _inst_1
[class_instances] (8) ?x_40 : ring ?x_38 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))) := @quotient_module.quotient.module ?x_41 ?x_42 ?x_43 ?x_44 ?x_45 ?x_46
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))) := @is_submodule.module ?x_47 ?x_48 ?x_49 ?x_50 ?x_51 ?x_52
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))) := @prod.module ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))) := @lc.module ?x_59 ?x_60 ?x_61 ?x_62
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))) := @vector_space.to_module ?x_63 ?x_64 ?x_65 ?x_66
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_67 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_68 ?x_69
[class_instances] (1) ?x_69 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_70 ?x_71
[class_instances] (0) ?x_67 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_68 ?x_69
[class_instances] (1) ?x_69 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_70 ?x_71
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))) := @ring.to_module ?x_67 ?x_68
failed is_def_eq
[class_instances] (8) ?x_40 : ring ?x_38 := @prod.ring ?x_41 ?x_42 ?x_43 ?x_44
[class_instances] (9) ?x_43 : ring ?x_41 := _inst_1
[class_instances] (9) ?x_44 : ring ?x_42 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))) := @quotient_module.quotient.module ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 ?x_50
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))) := @is_submodule.module ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 ?x_56
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))) := @prod.module ?x_57 ?x_58 ?x_59 ?x_60 ?x_61 ?x_62
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))) := @lc.module ?x_63 ?x_64 ?x_65 ?x_66
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))) := @vector_space.to_module ?x_67 ?x_68 ?x_69 ?x_70
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_71 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_72 ?x_73
[class_instances] (1) ?x_73 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_74 ?x_75
[class_instances] (0) ?x_71 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_72 ?x_73
[class_instances] (1) ?x_73 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_74 ?x_75
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))) := @ring.to_module ?x_71 ?x_72
failed is_def_eq
[class_instances] (9) ?x_44 : ring ?x_42 := @prod.ring ?x_45 ?x_46 ?x_47 ?x_48
[class_instances] (10) ?x_47 : ring ?x_45 := _inst_1
[class_instances] (10) ?x_48 : ring ?x_46 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))) := @quotient_module.quotient.module ?x_49 ?x_50 ?x_51 ?x_52 ?x_53 ?x_54
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))) := @is_submodule.module ?x_55 ?x_56 ?x_57 ?x_58 ?x_59 ?x_60
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))) := @prod.module ?x_61 ?x_62 ?x_63 ?x_64 ?x_65 ?x_66
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))) := @lc.module ?x_67 ?x_68 ?x_69 ?x_70
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))) := @vector_space.to_module ?x_71 ?x_72 ?x_73 ?x_74
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_75 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_76 ?x_77
[class_instances] (1) ?x_77 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_78 ?x_79
[class_instances] (0) ?x_75 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_76 ?x_77
[class_instances] (1) ?x_77 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_78 ?x_79
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))) := @ring.to_module ?x_75 ?x_76
failed is_def_eq
[class_instances] (10) ?x_48 : ring ?x_46 := @prod.ring ?x_49 ?x_50 ?x_51 ?x_52
[class_instances] (11) ?x_51 : ring ?x_49 := _inst_1
[class_instances] (11) ?x_52 : ring ?x_50 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))) := @quotient_module.quotient.module ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))) := @is_submodule.module ?x_59 ?x_60 ?x_61 ?x_62 ?x_63 ?x_64
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))) := @prod.module ?x_65 ?x_66 ?x_67 ?x_68 ?x_69 ?x_70
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))) := @lc.module ?x_71 ?x_72 ?x_73 ?x_74
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))) := @vector_space.to_module ?x_75 ?x_76 ?x_77 ?x_78
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_79 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_80 ?x_81
[class_instances] (1) ?x_81 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_82 ?x_83
[class_instances] (0) ?x_79 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_80 ?x_81
[class_instances] (1) ?x_81 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_82 ?x_83
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))) := @ring.to_module ?x_79 ?x_80
failed is_def_eq
[class_instances] (11) ?x_52 : ring ?x_50 := @prod.ring ?x_53 ?x_54 ?x_55 ?x_56
[class_instances] (12) ?x_55 : ring ?x_53 := _inst_1
[class_instances] (12) ?x_56 : ring ?x_54 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))) := @quotient_module.quotient.module ?x_57 ?x_58 ?x_59 ?x_60 ?x_61 ?x_62
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))) := @is_submodule.module ?x_63 ?x_64 ?x_65 ?x_66 ?x_67 ?x_68
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))) := @prod.module ?x_69 ?x_70 ?x_71 ?x_72 ?x_73 ?x_74
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))) := @lc.module ?x_75 ?x_76 ?x_77 ?x_78
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))) := @vector_space.to_module ?x_79 ?x_80 ?x_81 ?x_82
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_83 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_84 ?x_85
[class_instances] (1) ?x_85 : linear_ordered_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_86 ?x_87
[class_instances] (0) ?x_83 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_84 ?x_85
[class_instances] (1) ?x_85 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_86 ?x_87
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1 (@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))) := @ring.to_module ?x_83 ?x_84
failed is_def_eq
[class_instances] (12) ?x_56 : ring ?x_54 := @prod.ring ?x_57 ?x_58 ?x_59 ?x_60
[class_instances] (13) ?x_59 : ring ?x_57 := _inst_1
[class_instances] (13) ?x_60 : ring ?x_58 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))) := @quotient_module.quotient.module ?x_61 ?x_62 ?x_63 ?x_64 ?x_65 ?x_66
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))) := @is_submodule.module ?x_67 ?x_68 ?x_69 ?x_70 ?x_71 ?x_72
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))) := @prod.module ?x_73 ?x_74 ?x_75 ?x_76 ?x_77 ?x_78
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))) := @lc.module ?x_79 ?x_80 ?x_81 ?x_82
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))) := @vector_space.to_module ?x_83 ?x_84 ?x_85 ?x_86
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_87 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_88 ?x_89
[class_instances] (1) ?x_89 : linear_ordered_field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_90 ?x_91
[class_instances] (0) ?x_87 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_88 ?x_89
[class_instances] (1) ?x_89 : discrete_field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_90 ?x_91
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))) := @ring.to_module ?x_87 ?x_88
failed is_def_eq
[class_instances] (13) ?x_60 : ring ?x_58 := @prod.ring ?x_61 ?x_62 ?x_63 ?x_64
[class_instances] (14) ?x_63 : ring ?x_61 := _inst_1
[class_instances] (14) ?x_64 : ring ?x_62 := _inst_1
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))) := @quotient_module.quotient.module ?x_65 ?x_66 ?x_67 ?x_68 ?x_69 ?x_70
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))) := @is_submodule.module ?x_71 ?x_72 ?x_73 ?x_74 ?x_75 ?x_76
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))) := @prod.module ?x_77 ?x_78 ?x_79 ?x_80 ?x_81 ?x_82
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))) := @lc.module ?x_83 ?x_84 ?x_85 ?x_86
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))) := @vector_space.to_module ?x_87 ?x_88 ?x_89 ?x_90
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_91 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_92 ?x_93
[class_instances] (1) ?x_93 : linear_ordered_field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_94 ?x_95
[class_instances] (0) ?x_91 : field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_92 ?x_93
[class_instances] (1) ?x_93 : discrete_field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_94 ?x_95
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))) := @ring.to_module ?x_91 ?x_92
failed is_def_eq
[class_instances] (14) ?x_64 : ring ?x_62 := @prod.ring ?x_65 ?x_66 ?x_67 ?x_68
[class_instances] (15) ?x_67 : ring ?x_65 := _inst_1
[class_instances] (15) ?x_68 : ring ?x_66 := _inst_1
[class_instances] (1) ?x_10 : @module
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))))) := @quotient_module.quotient.module ?x_69 ?x_70 ?x_71 ?x_72 ?x_73 ?x_74
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))))) := @is_submodule.module ?x_75 ?x_76 ?x_77 ?x_78 ?x_79 ?x_80
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))))) := @prod.module ?x_81 ?x_82 ?x_83 ?x_84 ?x_85 ?x_86
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))))) := @lc.module ?x_87 ?x_88 ?x_89 ?x_90
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))))) := @vector_space.to_module ?x_91 ?x_92 ?x_93 ?x_94
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_95 : field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_96 ?x_97
[class_instances] (1) ?x_97 : linear_ordered_field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_98 ?x_99
[class_instances] (0) ?x_95 : field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_96 ?x_97
[class_instances] (1) ?x_97 : discrete_field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_98 ?x_99
[class_instances] cached failure for field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1)))))))))))))) := @ring.to_module ?x_95 ?x_96
failed is_def_eq
[class_instances] (15) ?x_68 : ring ?x_66 := @prod.ring ?x_69 ?x_70 ?x_71 ?x_72
[class_instances] (16) ?x_71 : ring ?x_69 := _inst_1
[class_instances] (16) ?x_72 : ring ?x_70 := _inst_1
[class_instances] (1) ?x_10 : @module
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))))) := @quotient_module.quotient.module ?x_73 ?x_74 ?x_75 ?x_76 ?x_77 ?x_78
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))))) := @is_submodule.module ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))))) := @prod.module ?x_85 ?x_86 ?x_87 ?x_88 ?x_89 ?x_90
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))))) := @lc.module ?x_91 ?x_92 ?x_93 ?x_94
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))))) := @vector_space.to_module ?x_95 ?x_96 ?x_97 ?x_98
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_99 : field
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @linear_ordered_field.to_field ?x_100 ?x_101
[class_instances] (1) ?x_101 : linear_ordered_field
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_102 ?x_103
[class_instances] (0) ?x_99 : field
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_field.to_field ?x_100 ?x_101
[class_instances] (1) ?x_101 : discrete_field
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) := @discrete_linear_ordered_field.to_discrete_field ?x_102 ?x_103
[class_instances] cached failure for field
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
[class_instances] cached failure for field
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
failed is_def_eq
[class_instances] (1) ?x_10 : @module
(↥S ×
↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
R
(@prod.ring ↥S
(↥S ×
↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S
(↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S)
_inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S × ↥S) _inst_1
(@prod.ring ↥S (↥S × ↥S) _inst_1
(@prod.ring ↥S ↥S _inst_1 _inst_1))))))))))))))) := @ring.to_module ?x_99 ?x_100
failed is_def_eq
[class_instances] (16) ?x_72 : ring ?x_70 := @prod.ring ?x_73 ?x_74 ?x_75 ?x_76
[class_instances] (17) ?x_75 : ring ?x_73 := _inst_1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment