mk_vsub_mk — Mathlib

English

For p1 = (a,b) and p2 = (c,d) in P × P', ((p1, p1') −ᵥ (p2, p2') : G × G') = (p1 −ᵥ p2, p1' −ᵥ p2').

Русский

Для p1=(a,b), p2=(c,d) выполняется ((p1,p1') −ᵥ (p2,p2') : G × G') = (p1 −ᵥ p2, p1' −ᵥ p2').

LaTeX

$$$$ ((p_1, p_1') -ᵥ (p_2, p_2') : G × G') = (p_1 -ᵥ p_2, p_1' -ᵥ p_2') $$$$

Lean4

@[simp]
theorem mk_vsub_mk (p₁ p₂ : P) (p₁' p₂' : P') : ((p₁, p₁') -ᵥ (p₂, p₂') : G × G') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂') :=
  rfl

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