def Mathlib.LibraryNote.«linking to library notes» : LibraryNote

You can now link to library notes!

Equations

• Mathlib.LibraryNote.«linking to library notes» = ()

def Mathlib.LibraryNote.«just like this» : LibraryNote

It works just like this!

Equations

• Mathlib.LibraryNote.«just like this» = ()

def hello : String

See note [linking to library notes].

In fact, See library Note [just like this].

Equations

• hello = "world"