Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 11:57 be0a4af2

View on Github →

chore(analysis): move real.angle to a dedicated file (#10065) We don't use this type anywhere else.

Estimated changes

added theorem real.angle.coe_add
added theorem real.angle.coe_coe_hom
added theorem real.angle.coe_neg
added theorem real.angle.coe_sub
added theorem real.angle.coe_two_pi
added theorem real.angle.coe_zero
added theorem real.angle.cos_sin_inj
added def real.angle
deleted theorem real.angle.coe_add
deleted theorem real.angle.coe_neg
deleted theorem real.angle.coe_sub
deleted theorem real.angle.coe_two_pi
deleted theorem real.angle.coe_zero
deleted theorem real.angle.cos_sin_inj
deleted def real.angle