Introducing notation

Stream: new members

[Jordan Brown]

What is the best way to introduce notation? I want to define Aut(E/F) to be the automorphism group of the field extension E of F, and Lean lets me write notation `Aut(` E `/` F `)`:= E \simeq\_a [F] E , but when I try to use this definition later it seems to not recognize something about the notation.

[Alex J. Best]

What exactly goes wrong later?

[Thomas Browning]

Here's an MWE:

import ring_theory.algebra

variables (F : Type*) [field F] (E : Type*) [field E] [algebra F E]

notation  `Aut(` E `/` F `)`:= E ≃ₐ[F] E

instance aut : group (Aut(E/F)) := {
    mul := λ ϕ ψ, ψ.trans ϕ,
    mul_assoc := λ ϕ ψ χ, rfl,
    one := 1,
    one_mul := λ ϕ, by {ext,refl},
    mul_one := λ ϕ, by {ext,refl},
    inv := alg_equiv.symm,
    mul_left_inv := λ ϕ, by {ext,exact alg_equiv.symm_apply_apply ϕ a},
}

When writing Aut(E/F), lean says : invalid definition, '|' or ':=' expected

[Patrick Massot]

You have precedences issues.

[Patrick Lutz]

How do you fix precedence issues?

[Patrick Massot]

I randomly add precedences numbers until Lean and I are both happy.

[Patrick Massot]

You can cheat by having a look at a similar notation definition.

[Kevin Buzzard]

I don't think I have ever seen round brackets being successfully used in notation

[Patrick Massot]

This is also true. I think I already failed to do that. But maybe I didn't try enough random numbers.