## Stream: new members

### Topic: Introducing notation

#### Jordan Brown (Aug 04 2020 at 21:00):

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 (Aug 04 2020 at 21:22):

What exactly goes wrong later?

#### Thomas Browning (Aug 04 2020 at 21:28):

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 (Aug 04 2020 at 21:29):

You have precedences issues.

#### Patrick Lutz (Aug 04 2020 at 21:30):

How do you fix precedence issues?

#### Patrick Massot (Aug 04 2020 at 21:30):

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

#### Patrick Massot (Aug 04 2020 at 21:31):

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

#### Kevin Buzzard (Aug 04 2020 at 21:40):

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

#### Patrick Massot (Aug 04 2020 at 21:40):

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

Last updated: Dec 20 2023 at 11:08 UTC