Zulip Chat Archive

Stream: Is there code for X?

Topic: Hyperbolic Trig Functions


view this post on Zulip James Arthur (Aug 14 2020 at 12:59):

I was looking through the list of UG Mathematics that isn't in mathlib and it says that hyperbolic trig functions aren't implemented. Is this still up to date?

view this post on Zulip Shing Tak Lam (Aug 14 2020 at 13:02):

https://leanprover-community.github.io/undergrad_todo.html#5-7 probably has a missing "and".

cosh and sinh is already there, I assume "reciprocal hyperbolic trigonometric functions" is referring to sec, cosec, cot, sech, cosech and coth, which I don't think is in mathlib yet.

view this post on Zulip Patrick Massot (Aug 14 2020 at 13:12):

No it refers to https://en.wikipedia.org/wiki/Inverse_hyperbolic_functions

view this post on Zulip James Arthur (Aug 14 2020 at 13:19):

That's even cooler! Thankyou.

view this post on Zulip James Arthur (Aug 15 2020 at 17:29):

I have some code wrt to arsinh. Do you want it for mathlib? I should probably also do cosh before any sort of PR

view this post on Zulip Johan Commelin (Aug 15 2020 at 17:35):

As I said before, it's good to start with small PRs

view this post on Zulip Johan Commelin (Aug 15 2020 at 17:35):

@James Arthur :up:

view this post on Zulip James Arthur (Aug 15 2020 at 17:38):

I'll pull request my sinh stuff then!

view this post on Zulip James Arthur (Aug 15 2020 at 17:38):

Ah, once I've also fiddled with my code via the style guide

view this post on Zulip Johan Commelin (Aug 15 2020 at 17:48):

That's exactly why I suggest starting with a small PR :wink: :smiley:

view this post on Zulip James Arthur (Aug 15 2020 at 17:57):

The style guide is looooong!

view this post on Zulip James Arthur (Aug 18 2020 at 10:33):

With respect to Hyperbolic Trig, would it be nice to move all of the definitions into their own file? i.e. HypTrig.lean or something. Unfortunately I would believe it would break a load of imports.

view this post on Zulip James Arthur (Aug 18 2020 at 10:33):

As they are all currently under exponential.lean and they look slightly out of place.

view this post on Zulip Ruben Van de Velde (Aug 18 2020 at 10:46):

Probably not with a CamelCase name, but that generally sounds like a good idea to me

view this post on Zulip Johan Commelin (Aug 18 2020 at 10:54):

I don't think it will break much. Those functions haven't been used that much so far, right?

view this post on Zulip James Arthur (Aug 18 2020 at 11:01):

Sorry, I have a thing for camel case, would 'hyp_trig.lean' be better?

view this post on Zulip James Arthur (Aug 18 2020 at 11:02):

Johan Commelin said:

I don't think it will break much. Those functions haven't been used that much so far, right?

I can always make a pull request and fix from there

view this post on Zulip James Arthur (Aug 18 2020 at 11:02):

It would only be donky work of changing imports, perfect for me!


Last updated: May 19 2021 at 00:40 UTC