Eric Wieser

I've learnt my lesson - I should target master, not the versioned releases in future

Just rebased this, as I was running into the issue again. Would appreciate some feedback on whether the idea sounds good. ~~If it does, then I'll try to add a...

Your mistake is that you use `math.pi` which is only an approximation of `sympy.pi`

Can you share the exact code you're using for 2 ?

Yes, as soon as you use the `math` module you are working with floating-point approximations and not symbolic calculations. Note you can paste code directly into comments here by using...

Indeed, the function referred to by @Greg1950 can be found [in the docs here](https://galgebra.readthedocs.io/en/latest/generated/galgebra.mv.html#galgebra.mv.rot)

The meaning of the `hint` argument is described [in the docs for `exp`](https://galgebra.readthedocs.io/en/latest/generated/galgebra.mv.html#galgebra.mv.Mv.exp): https://github.com/pygae/galgebra/blob/3a53b29fb141be1ae47d8df8fc7005c10869cded/galgebra/mv.py#L1093-L1100

My guess would be that geany is using an old version of python on your system; if you run a program that prints `sys.executable`, you can compare which versions are...

It looks like you've accidentally rebased master on top of your branch, as there are 170 commits now!

Closing, since this was implemented in https://github.com/leanprover-community/mathlib4/pull/7790