## Stream: general

### Topic: What is a parent structure?

#### Chris Hughes (Aug 03 2019 at 18:50):

Why doesn't this work

import ring_theory.algebra

structure alg_equiv (α β γ : Type*) [comm_ring α] [ring β] [ring γ]
[algebra α β] [algebra α γ] extends @alg_hom α β γ _ _ _ _ _ :=
--invalid 'structure', expression must be a 'parent' structure


#### Kevin Buzzard (Aug 03 2019 at 18:58):

That's a bit annoying isn't it! My impression is that Lean chokes on the @ symbol and doesn't go any further.

structure foo (α : Type) :=
(hello_mum : ℕ)

structure bar (α : Type) extends @foo α := -- same error
(hello_world : bool)


#### Kevin Buzzard (Aug 03 2019 at 18:59):

You could of course just work around it by putting the fields in and making the projection yourself. Are there any serious disadvantages to this other than it being a bore?

#### Chris Hughes (Aug 03 2019 at 19:00):

I think the best solution is to make that field of alg_hom explicit. Then using the notation should work

#1296

#### Kevin Buzzard (Aug 03 2019 at 22:05):

6^4

Last updated: May 12 2021 at 23:13 UTC