Fundamental period of sin

Stream: Is there code for X?

[Jiatong Yang]

Is there code asserting that the fundamental period of the real sine function is 2π?

[Daniel Weber]

There's docs#Real.sin_periodic, but that's not the fundamental period

[Daniel Weber]

I think it shouldn't be hard to get from docs#Real.sin_eq_one_iff

[Joachim Breitner]

This topic's title could also be the name of some serious piece of world literature.