## 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):

@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: May 19 2021 at 00:40 UTC