-
-
Save kbuzzard/0d90aae44ce2034af134400be2065d0a to your computer and use it in GitHub Desktop.
pp.all is off, this is the error I'm getting
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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