angle): `induction_on` (#11886)

Commit

3 years ago

feat(analysis/special_functions/trigonometric/angle): `induction_on` (#11886) Add `real.angle.induction_on`, for use in deducing results for `real.angle` from those for `ℝ`.

Author

jsm28

Parents

26179ccd

mathlib 98ef84ef - feat(analysis/special_functions/trigonometric/angle): `induction_on` (#11886)

mathlib
98ef84ef - feat(analysis/special_functions/trigonometric/angle): `induction_on` (#11886)