cos_toReal — Mathlib

English

For any angle θ, cos of its real representative equals the cosine of the angle: cos(θ.toReal) = cos θ.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem cos_toReal (θ : Angle) : Real.cos θ.toReal = cos θ := by conv_rhs => rw [← coe_toReal θ, cos_coe]

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