unicode in defs

Stream: condensed mathematics

[Kevin Buzzard]

We have stuff like

def ϕ : ℒ S → ℒ S := ...

and other examples in src/laurent_measures/. Is this OK? I think Mario warned us against unicode in defs?

[Johan Commelin]

Ooh, I maybe wouldn't do this in mathlib, but I think it's totally fine for this repo

[Kevin Buzzard]

Is

def r : ℝ≥0 := (1 / 2) ^ (p:ℝ)

in the root namespace OK?

[Yaël Dillies]

25 lettes in the alphabet ae enough!