Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/rw_failure Secret

Created May 7, 2021 20:18
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/0d90aae44ce2034af134400be2065d0a to your computer and use it in GitHub Desktop.
Save kbuzzard/0d90aae44ce2034af134400be2065d0a to your computer and use it in GitHub Desktop.
Download ZIP
pp.all is off, this is the error I'm getting
Raw
rw_failure
invalid type ascription, term has type
@has_mem.mem
(@coe_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@submodule
(@coe_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(Gᵢ a).to_add_comm_group)
(@direct_sum.has_add_subgroup_decomposition.module A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a))
(@set_like.has_mem
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(Gᵢ a).to_add_comm_group)
(@direct_sum.has_add_subgroup_decomposition.module A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a))
(@coe_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@submodule.set_like
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(Gᵢ a).to_add_comm_group)
(@direct_sum.has_add_subgroup_decomposition.module A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a)))
(@has_scalar.smul
(@coe_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@smul_with_zero.to_has_scalar
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@mul_zero_class.to_has_zero
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@mul_zero_one_class.to_mul_zero_class
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@monoid_with_zero.to_mul_zero_one_class
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@semiring.to_monoid_with_zero
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))))))
(@add_zero_class.to_has_zero
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@add_monoid.to_add_zero_class
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@add_comm_monoid.to_add_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@add_comm_group.to_add_comm_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(Gᵢ a).to_add_comm_group))))
(@mul_action_with_zero.to_smul_with_zero
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@semiring.to_monoid_with_zero
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5)))
(@add_zero_class.to_has_zero
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@add_monoid.to_add_zero_class
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@add_comm_monoid.to_add_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@add_comm_group.to_add_comm_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(Gᵢ a).to_add_comm_group))))
(@module.to_mul_action_with_zero
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ a))
(Gᵢ a).to_add_comm_group)
(@direct_sum.has_add_subgroup_decomposition.module A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a))))
(@coe_fn
(@add_monoid_hom
(@direct_sum A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
0)
(@add_monoid.to_add_zero_class
(@direct_sum A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))
(@add_comm_monoid.to_add_monoid
(@direct_sum A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))
(@direct_sum.add_comm_monoid A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))))
(@add_monoid.to_add_zero_class
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
0)
(@add_comm_monoid.to_add_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
0)
((λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
0))))
(@add_monoid_hom.has_coe_to_fun
(@direct_sum A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
0)
(@add_monoid.to_add_zero_class
(@direct_sum A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))
(@add_comm_monoid.to_add_monoid
(@direct_sum A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))
(@direct_sum.add_comm_monoid A
(λ (i : A),
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(λ (i : A),
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
i))))
(@add_monoid.to_add_zero_class
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
0)
(@add_comm_monoid.to_add_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
0)
((λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
0))))
(@direct_sum.projection A (λ (a b : A), _inst_1 a b)
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
(λ (i : A),
@add_comm_group.to_add_comm_monoid
((λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
i)
(Gᵢ i).to_add_comm_group)
0)
(@coe_fn
(@ring_equiv R
(@direct_sum A
(λ (i : A),
@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ i))
(λ (i : A),
@add_comm_group.to_add_comm_monoid
(@coe_sort (@add_subgroup R (@add_comm_group.to_add_group R …)) … …)
…))
…
…
…
…)
…
…
…))
m)
M
but is expected to have type
@has_mem.mem
(@coe_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
(@set_like.has_coe_to_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
R
(@submodule.set_like
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))))
(@direct_sum.has_add_subgroup_decomposition.component_submodule_for_zero_component_subring A
(λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a))
(@submodule
(@coe_sort
(@add_subgroup R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
(@set_like.has_coe_to_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
R
(@submodule.set_like
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))))
(@direct_sum.has_add_subgroup_decomposition.component_submodule_for_zero_component_subring A
(λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@direct_sum.has_add_subgroup_decomposition.component_submodule_for_zero_component_subring A
(λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a).add_comm_monoid
(@direct_sum.has_add_subgroup_decomposition.component_submodule_for_zero_component_subring A
(λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a).module)
(@set_like.has_mem
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@coe_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
(@set_like.has_coe_to_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
R
(@submodule.set_like
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))))
(@direct_sum.has_add_subgroup_decomposition.component_submodule_for_zero_component_subring A
(λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a))
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@direct_sum.has_add_subgroup_decomposition.component_submodule_for_zero_component_subring A
(λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a).add_comm_monoid
(@direct_sum.has_add_subgroup_decomposition.component_submodule_for_zero_component_subring A
(λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5
a).module)
(@coe_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
(@set_like.has_coe_to_sort
(@submodule
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
(@comm_ring.to_ring R _inst_3)
Gᵢ
_inst_4
_inst_5))
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))
(@algebra.to_module
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@comm_ring.to_comm_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
(@direct_sum.has_add_subgroup_decomposition.comm_ring A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5))
(@ring.to_semiring R (@comm_ring.to_ring R _inst_3))
(@direct_sum.has_add_subgroup_decomposition.algebra A (λ (a b : A), _inst_1 a b)
(@sub_neg_monoid.to_add_monoid A (@add_group.to_sub_neg_monoid A _inst_2))
R
_inst_3
Gᵢ
_inst_4
_inst_5)))
R
(@submodule.set_like
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3)))))
(Gᵢ 0))
R
(@ring.to_semiring
(@coe_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
(@set_like.has_coe_to_sort
(@add_subgroup R
(@add_comm_group.to_add_group R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_3))))
R
(@add_subgroup.set_like R (@add_comm_group.to_add_group R (@ring.to_add_comm_group R …))))
…)
…)
…
…))
…)
…)
…
M
state:
A : Type u_1,
_inst_1 : decidable_eq A,
_inst_2 : add_group A,
R : Type u_2,
_inst_3 : comm_ring R,
Gᵢ : A → add_subgroup R,
_inst_4 : has_add_subgroup_decomposition Gᵢ,
_inst_5 : add_subgroup.is_gmonoid Gᵢ,
a : A,
M : submodule ↥(Gᵢ 0) ↥(Gᵢ a),
M' : submodule ↥(Gᵢ 0) R := submodule.map (component_submodule_for_zero_component_subring R Gᵢ a).subtype M,
f : ↥(Gᵢ a) →₀ R,
hm : ⇑(finsupp.total ↥(Gᵢ a) R R ⇑((Gᵢ a).subtype)) f ∈ Gᵢ a,
hm' :
f.sum
(λ (m : ↥(Gᵢ a)) (b : R),
⇑((Gᵢ a).subtype)
(⇑(projection (λ (i : A), ↥(Gᵢ i)) a)
(⇑(of (λ (i : A), ↥(Gᵢ i)) 0)
(⇑(projection (λ (i : A), ↥(Gᵢ i)) 0) (⇑(add_subgroup_decomposition_ring_equiv Gᵢ) b)) *
⇑(of (λ (i : A), ↥(Gᵢ i)) a) m))) =
⇑(finsupp.total ↥(Gᵢ a) R R ⇑((Gᵢ a).subtype)) f,
m : ↥(Gᵢ a),
hm : m ∈ f.support,
hf : ↑(f.support) ⊆ ↑M
⊢ ⇑(projection (λ (i : A), ↥(Gᵢ i)) 0) (⇑(add_subgroup_decomposition_ring_equiv Gᵢ) (⇑f m)) • m ∈ M
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment