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"