Zulip Chat Archive
Stream: Is there code for X?
Topic: Hyperbolic Trig Functions
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?
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.
Patrick Massot (Aug 14 2020 at 13:12):
No it refers to https://en.wikipedia.org/wiki/Inverse_hyperbolic_functions
James Arthur (Aug 14 2020 at 13:19):
That's even cooler! Thankyou.
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
Johan Commelin (Aug 15 2020 at 17:35):
As I said before, it's good to start with small PRs
Johan Commelin (Aug 15 2020 at 17:35):
@James Arthur :up:
James Arthur (Aug 15 2020 at 17:38):
I'll pull request my sinh stuff then!
James Arthur (Aug 15 2020 at 17:38):
Ah, once I've also fiddled with my code via the style guide
Johan Commelin (Aug 15 2020 at 17:48):
That's exactly why I suggest starting with a small PR :wink: :smiley:
James Arthur (Aug 15 2020 at 17:57):
The style guide is looooong!
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.
James Arthur (Aug 18 2020 at 10:33):
As they are all currently under exponential.lean and they look slightly out of place.
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
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?
James Arthur (Aug 18 2020 at 11:01):
Sorry, I have a thing for camel case, would 'hyp_trig.lean' be better?
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
James Arthur (Aug 18 2020 at 11:02):
It would only be donky work of changing imports, perfect for me!
Last updated: Dec 20 2023 at 11:08 UTC