Mathlib semantic search suggests: a trigonometry typeclass

Stream: general

[Kevin Buzzard]

Eric Wieser said:

I searched for "sine rule" and the autoformalization was

theorem sin_cos_eq_sin_cos_of_cos_eq_cos {α : Type*} [inhabited α] [discrete_linear_ordered_field α]
  [trigonometry α] {a b c : α} (h : cos a = cos b) :
  sin a * cos c = sin b * cos c ↔ sin a = sin b

Should we introduce a [trigonometry α] typeclass to generalize over complex.sin and real.sin?

is_R_or_C.sin

[Kevin Buzzard]

Because $\sin(\overline{z})=\overline{\sin(z)}$ you could even do it for my preferred variant (the fields which are finite $\R$-algebras)

[Eric Wieser]

Is it canonical to define $\operatorname{sin} x$ on any topological algebra as the RHS of docs#real.sin_eq_tsum?

[Kevin Buzzard]

Re sin: That's how exp works in the p-adics but sin and cos are less useful in that setting.

[Notification Bot]

A message was moved here from #general > Mathlib semantic search by Eric Wieser.