Meromorphicity of Complex.tan and Complex.tanh

theorem Complex.meromorphicNFOn_tan : MeromorphicNFOn tan Set.univ

The function tan is meromorphic in normal form on Set.univ.

theorem Complex.meromorphicAt_tan (z : ℂ) : MeromorphicAt tan z

The function tan is meromorphic at any z.

theorem Complex.meromorphic_tan : Meromorphic tan

The function tan is meromorphic.

theorem Complex.meromorphicNFOn_tanh : MeromorphicNFOn tanh Set.univ

The function tanh is meromorphic in normal form on Set.univ.

theorem Complex.meromorphicAt_tanh (z : ℂ) : MeromorphicAt tanh z

The function tanh is meromorphic at any z.

theorem Complex.meromorphic_tanh : Meromorphic tanh

The function tanh is meromorphic.