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

[Laurance Lau]

Kevin Buzzard said:

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

I think that seems good on its own. However, some existing lemmas (e.g. Real.cos_pi_div_three) have just pi divided by something. If we are to be consistent in ordering the operations, then maybe we would also say 1 / 3 * \pi which seems a bit extra...

[Laurance Lau]

Aaron Liu said:

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

Continued, since the argument of sin isn't the full rotation, perhaps mul should be inserted. Then again I'm not sure that this two_pi rule is codified anywhere other than just existing convention or if there's some well-thought-out motivation for omitting it in the first place.

[Violeta Hernández]

the obvious solution is to rewrite everything in terms of τ