Is there a way to specify fields that allow stars?

Stream: Is there code for X?

[Mr Proof]

In my code I want to define a norm in the form AA+BB+CC*+...

def Octonion.norm {α : Type} [Field α](p: 𝕆[α])  : α :=
  p.re* p.re + p.e1*p.e1 + p.e2*p.e2 + p.e3*p.e3 + p.e4*p.e4 + p.e5*p.e5 + p.e6*p.e6 + p.e7*p.e7

I want to change it so that it reads p.re*(star p.re)+ ...
but it won't allow this. Is there a way to specify it accepts fields with the star operation defined?

Alternatively I would have something like p.re.norm + p.e1.norm + .... if the norm (squared magnitude) was defined for each field.

[Eric Wieser]

you want to add [StarRing α] most likely (after the existing Field α that you have)

[Eric Wieser]

You could of course just add [Star α], but that allows a nonsensical definition

[Mr Proof]

Hmm... it's still saying "failed to synthesize" when it gets to (star..) Not sure why..

import Mathlib

/-

An definition of the Octonion Algebra over field F denoted by 𝕆[F]

-/

structure Octonion (α : Type u) where
  re: α
  e1: α
  e2: α
  e3: α
  e4: α
  e5: α
  e6: α
  e7: α

/- Notation and output -/

notation "𝕆" => Octonion ℝ

notation "𝕆[" F "]" => Octonion F



/- conjugation-/
def Octonion.star {α : Type} [Field α] (p : 𝕆[α]) : Octonion α :={
    re := p.re
    e1 := -p.e1
    e2 := -p.e2
    e3 := -p.e3
    e4 := -p.e4
    e5 := -p.e5
    e6 := -p.e6
    e7 := -p.e7
}


def Octonion.norm {α : Type} [Field α] [StarRing α] (p: 𝕆[α])  : α :=
  p.re* (star p.re) + p.e1* (star p.e1) + p.e2* (star p.e2) + p.e3* (star p.e3) + p.e4* (star p.e4) + p.e5*(star p.e5) + p.e6*(star p.e6) + p.e7*(star p.e7)

[Eric Wieser]

Can you make a #mwe, or at least paste the full message?

[Mr Proof]

(See above). I see the problem. My definition of Octonion.star is somehow interfering with that star . If I delete the Octonion.star definition then it works. Is it a scoping issue?

If I swap the order of those two definitions then it works. But that doesn't seem the best solution.

[Eric Wieser]

You should mark Octonion.star as protected

[Eric Wieser]

Or eliminate it entirely, and inline the definition into instance : Star (Octonion _) where star o := sorry

[Mr Proof]

Perhaps its confusing itself because if I did 𝕆[𝕆] then I better make sure 𝕆 is also a star ring. But your solution works.

[Eric Wieser]

Independent of your confusion, you will definitely want to show StarRing 𝕆 later anyway, assuming it's true!