instZeroEuclideanQuadrant

Mathlib.Geometry.Manifold.Instances.Real

URI: https://scilib.ai/kg/mathlib#instZeroEuclideanQuadrant

English

The origin belongs to EuclideanQuadrant n, i.e. the all-zero vector is in the quadrant.

Русский

Начало координат принадлежит Евклидову квадранту: вектор нулей лежит в квадранте.

LaTeX

$$$$\mathbf{0} = (0,\dots,0) \in Q_n.$$$$

Lean4

instance {n : ℕ} : Zero (EuclideanQuadrant n) :=
  ⟨⟨fun _ ↦ 0, by simp⟩⟩

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

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

Разделы

Аффилиация

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