vsub_ne_zero

Mathlib.Algebra.AddTorsor.Defs

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

English

p -ᵥ q ≠ 0 iff p ≠ q.

Русский

p -ᵥ q ≠ 0 тогда и только тогда, когда p ≠ q.

LaTeX

$$$vsub(p_1,p_2) \neq 0_G \iff p_1 \neq p_2$$$

Lean4

theorem vsub_ne_zero {p q : P} : p -ᵥ q ≠ (0 : G) ↔ p ≠ q :=
  not_congr vsub_eq_zero_iff_eq

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

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

Разделы

Аффилиация

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