Zulip Chat Archive

Stream: new members

Topic: Introducing notation


view this post on Zulip 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.

view this post on Zulip Alex J. Best (Aug 04 2020 at 21:22):

What exactly goes wrong later?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 04 2020 at 21:29):

You have precedences issues.

view this post on Zulip Patrick Lutz (Aug 04 2020 at 21:30):

How do you fix precedence issues?

view this post on Zulip Patrick Massot (Aug 04 2020 at 21:30):

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

view this post on Zulip Patrick Massot (Aug 04 2020 at 21:31):

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:40):

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

view this post on Zulip 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: May 13 2021 at 21:12 UTC