Skip to content

Commit

Permalink
feat: port Analysis.SpecialFunctions.Trigonometric.Angle (#4040)
Browse files Browse the repository at this point in the history
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
  • Loading branch information
pechersky and ChrisHughes24 committed May 17, 2023
1 parent d25807f commit 8886682
Show file tree
Hide file tree
Showing 3 changed files with 1,066 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Expand Up @@ -433,6 +433,7 @@ import Mathlib.Analysis.Seminorm
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Polynomials
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev
import Mathlib.Analysis.SpecificLimits.Basic
Expand Down

0 comments on commit 8886682

Please sign in to comment.