sin_toReal — Mathlib

English

For any angle θ, sin of its real representative equals the sine of the angle itself: sin(θ.toReal) = sin θ.

Русский

Для любого угла θ синус реального представления угла равен синусу самого угла: sin(θ.toReal) = sin θ.

LaTeX

$$$\sin(\theta^{\mathrm{toReal}}) = \sin \theta$$$

Lean4

@[simp]
theorem sin_toReal (θ : Angle) : Real.sin θ.toReal = sin θ := by conv_rhs => rw [← coe_toReal θ, sin_coe]

Похожие утверждения