Mathlib trivia question (difficulty: hard maybe)

Stream: general

[Mason McBride]

Does anyone know the lean video seminar/video on youtube that discusses the syntax of the liouville number? I want a link to watch that talk again. File: https://github.com/leanprover-community/mathlib4/blob/c6979569edc545f999b82d8a833b190c918aec2e/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean

[Mason McBride]

def liouvilleNumber (m : ℝ) : ℝ :=
∑' i : ℕ, 1 / m ^ i !

I can't find backtick on mobile

[Kevin Buzzard]

Are you really asking about the syntax of this number? What do you mean?

[Mason McBride]

There was a talk where the speaker discussed the "shortcuts" that lean is using to make the syntax clean and I want to see it again.

[Mason McBride]

what's the apostrophe on the sigma

[Mason McBride]

The answer to my trivia question is the link to the youtube video

[Kevin Buzzard]

If you have that lean code running in VS Code on your machine then you can hover over the apostrophe to find out what it means. In this case I think it means that Sigma was already taken to mean sum over a finite set so new notation was needed for convergent infinite sum.