oangle_zero_left

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

URI: https://scilib.ai/kg/mathlib#Orientation.oangle_zero_left

English

If the first vector is zero, the oriented angle is zero: o.oangle(0, y) = 0.

Русский

Если первый вектор равен нулю, ориентированный угол равен нулю: o.oangle(0, y) = 0.

LaTeX

$$$o.oangle(0,y) = 0$$$

Lean4

/-- If the first vector passed to `oangle` is 0, the result is 0. -/
@[simp]
theorem oangle_zero_left (x : V) : o.oangle 0 x = 0 := by simp [oangle]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru