Naming of trigonometric identities

Stream: mathlib4

[Laurance Lau]

Hello all, I would like to know which of the following would be preferred:
lemma sin_two_mul_pi_div_three : sin (2 * π / 3) = √3 / 2 := by sorry
lemma sin_pi_mul_two_div_three : sin (π * 2 / 3) = √3 / 2 := by sorry

PR #32389

[Kevin Buzzard]

I think I would have gone for 2 / 3 * \pi! i.e. (number) * pi

[Kevin Buzzard]

although 2 * pi seems to be a special case e.g. docs#Real.cos_nat_mul_two_pi_sub , so the first one is also reasonable. The second is is kind of horrible :-)

[Aaron Liu]

how about sin_two_pi_div_three treating 2pi as a single "unit" (the full rotation)

[Weiyi Wang]

We are this close to sin_tau_div_three :laughing:

[Laurance Lau]

Aaron Liu said:

how about sin_two_pi_div_three treating 2pi as a single "unit" (the full rotation)

It does seem that for two_pi only mul is routinely omitted. Provided that this is one lemma out of a collection of related lemmas, would you also go for sin_three_pi_div_four?

[Aaron Liu]

I'm somewhat less supportive of that one