tan_oangle_add_right_smul_rotation_pi_div_two

English

For x ≠ 0 and r ∈ R, tan o.oangle(x, x + r·rotation(π/2)x) = r.

Русский

Для x ≠ 0 и r ∈ R, tan(о.oangle(x, x + r·rotation(π/2)x)) = r.

LaTeX

$$$ \tan\left(o.oangle\left(x, x + r\cdot rotation\left(\frac{\pi}{2}\right)x\right)\right) = r $$$

Lean4

/-- The tangent of an angle in a right-angled triangle, where one side is a multiple of a
rotation of another by `π / 2`. -/
theorem tan_oangle_add_right_smul_rotation_pi_div_two {x : V} (h : x ≠ 0) (r : ℝ) :
    Real.Angle.tan (o.oangle x (x + r • o.rotation (π / 2 : ℝ) x)) = r := by
  rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]

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