## Stream: new members

### Topic: field already declared

#### Horatiu Cheval (Feb 17 2021 at 08:25):

I am trying to define a small algebraic hierarchy from scratch following the way it's done in mathlib and I get this error.

class monoid (M : Type*) extends has_mul M, has_one M :=
(mul_assoc : ∀ x y z : M, x * (y * z) = (x * y) * z)
(mul_one : ∀ x : M, x * 1 = x)
(one_mul : ∀ x : M, 1 * x = x)

class comm_monoid (M : Type*) extends monoid M :=
(mul_comm : ∀ x y : M, x * y = x * y)

class group (G : Type*) extends monoid G, has_inv G :=
(mul_left_inv : ∀ x : G, x⁻¹ * x = 1)

class comm_group (G : Type*) extends group G, comm_monoid G

--invalid 'structure' header, field 'to_monoid' from 'hidden.comm_monoid' has already been declared


I assume it's because both group and comm_monoid have to_monoid fields, but how do I fix it?

#### Johan Commelin (Feb 17 2021 at 08:26):

You can use

set_option old_structure_cmd true


before your code

#### Johan Commelin (Feb 17 2021 at 08:27):

This will merge the fields that both parents have in common

#### Johan Commelin (Feb 17 2021 at 08:27):

But the structures that you extend should also be "old" structures. So you have to set the option all the way at the top

#### Horatiu Cheval (Feb 17 2021 at 08:28):

Oh, I see, I missed that from the mathlib source files. Thanks!

Last updated: May 18 2021 at 17:44 UTC