Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 19:27 78b323bc

View on Github →

feat(analysis/special_functions/trigonometric): inequality tan x > x (#12352)

Estimated changes

deleted theorem real.sin_gt_sub_cube
deleted theorem real.sin_lt
added theorem real.deriv_tan_sub_id
added theorem real.lt_tan
added theorem real.sin_gt_sub_cube
added theorem real.sin_lt