## Stream: general

### Topic: lean and latex

#### Kevin Buzzard (Dec 26 2020 at 18:40):

I want to be able to mix Lean code and math mode within a LaTeX document. I am writing calculations about Bernoulli numbers where everything happening in nat I want to be in lstlean and everything in $\mathbb{Q}$ I want to be in $\sum_{i+j=n}c_iB_i$ maths mode. Ultimately it means that I would like to have lstlean working in numerators of LaTeX \frac{<numerators>}{<denominators>}s and _{<subscripts>}. Or should I just use some kind of tt mode, \mathtt or something? I have no understanding of what is actually going on here but this sort of trick seems to be a kind of cool way of keeping a rational $/$ distinguished from a natural / and similarly for -.

#### Mario Carneiro (Dec 26 2020 at 18:41):

I would just fake it using \mathtt and \color

better.png

#### Kevin Buzzard (Dec 26 2020 at 18:46):

maths mode eats the spaces in the lean

#### Mario Carneiro (Dec 26 2020 at 18:47):

\mbox{\texttt{...}} might help with that

#### Mario Carneiro (Dec 26 2020 at 18:48):

you might even be able to use lstlean in there, not sure

#### Kevin Buzzard (Dec 26 2020 at 18:53):

Nice --

$\sum_{(i,j)\in\mbox{\lstinline{antidiagonal n}}}\frac{\mbox{\lstinline{pascal i j}}}{\mbox{\lstinline{j.succ}}}B_i = 1.$


gives me
nice.png

#### Kevin Buzzard (Dec 26 2020 at 18:55):

The Lean font is a tiny bit too big compared to the maths font. The Lean n is bigger than the maths $(i,j)$.

#### Rob Lewis (Dec 26 2020 at 19:00):

At some point I modified my local lstlean.tex to scale things down slightly (in the whole document, not just math mode):

% Default style fors listingsred
lineskip={-1.5pt},
basicstyle={\ttfamily\scalefont{.95}},


You could probably make a macro for \mbox{\lstinline that passes a basicstyle that scales it down.

#### Kevin Buzzard (Dec 26 2020 at 19:01):

Can I get something like that in the docs? It's some theorem about Bernoulli numbers which I have in some branch of mathlib. I don't even know if it's the right way to document it, I've just been goofing around with writing some stuff up in LaTeX.

#### Rob Lewis (Dec 26 2020 at 19:07):

I think it's dangerous to use formatting tricks to convey semantic info in the docs. Even if the trick were used uniformly through all the doc pages, people showing up on a random page won't necessarily pick up on that. If there's something important to point out about the division maybe it's better to spell it out.

#### Rob Lewis (Dec 26 2020 at 19:08):

I don't object to the styling though.

Last updated: May 17 2021 at 21:12 UTC