sub_snd — Mathlib

English

Let x, y ∈ C⋆ᵐᵒᵈ(A, E × F). Then the second component of their difference is the difference of their second components: (x − y).snd = x.snd − y.snd.

Русский

Пусть x, y ∈ C⋆ᵐᵒᵈ(A, E × F). Тогда вторая координата разности равна разности вторых координат: (x − y).snd = x.snd − y.snd.

LaTeX

$$$$ (x - y).snd = x.snd - y.snd $$$$

Lean4

@[simp]
theorem sub_snd : (x - y).snd = x.snd - y.snd :=
  rfl

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