## Stream: general

### Topic: Proving that a structure is an add_comm_group

#### Youjack (Sep 28 2022 at 01:40):

Suppose I have a structure

structure mystruct :=
(a : ℝ)
(b : ℝ)


Is there an easy way to prove this?

instance : add_comm_group mystruct := sorry


I know that there is a prod.add_comm_group in mathlib, but I don't know how to apply this to mystruct.
Maybe I should use prod ℝ ℝ instead of mystruct, but I would like to extends mystruct later, so I prefer using structure.

#### Kyle Miller (Sep 28 2022 at 06:05):

For what it's worth, docs#prod is a structure that you can extend.

#### Kyle Miller (Sep 28 2022 at 06:08):

Regarding defining an add_comm_group structure on mystruct using an equivalence mystruct ≃ prod ℝ ℝ, I thought that mathlib had a way to transfer such a structure over an equivalence but I can't find it at the moment.

#### Yaël Dillies (Sep 28 2022 at 06:47):

Write the obvious function mystruct → ℝ × ℝ then show it's injective and finally use docs#function.injective.add_comm_group.

#### Jireh Loreaux (Sep 28 2022 at 06:50):

Note: you have to define all the data fields first.

#### Yaël Dillies (Sep 28 2022 at 06:52):

Alternatively, use tactic#equiv_rw.

#### Notification Bot (Sep 28 2022 at 07:08):

Youjack has marked this topic as resolved.

#### Notification Bot (Sep 28 2022 at 07:08):

Youjack has marked this topic as unresolved.

#### Youjack (Sep 28 2022 at 07:50):

I make it with equiv.add_comm_group

import data.real.basic
import logic.equiv.transfer_instance

structure mystruct :=
(a : ℝ)
(b : ℝ)

def mystruct_equiv_prod : mystruct ≃ (ℝ × ℝ) := {
to_fun  := λ s, (s.a, s.b),
inv_fun := λ p, ⟨p.1, p.2⟩,
left_inv  := λ s, match s with | ⟨_,_⟩ := rfl end,
right_inv := λ _, prod.mk.eta
}