Mathlib Phrasebook

22. Trigonometric functions🔗

Mathlib contains definitions for the standard trigonometric functions. We outline some related theory here.

To get some notation below we first open a scope:

open scoped Real
  1. 22.1. Basic definitions
  2. 22.2. Basic properties
  3. 22.3. Special values and identities