constVAdd_zero — Mathlib

English

For any G and P with a torsor structure, constVAdd P (0) = 1, i.e., the constant translation by zero is the identity permutation.

Русский

Для любой группы G и множества P с тorsорной структурой константная добавка нулевого элемента действует как тождество.

LaTeX

$$$$ \text{constVAdd } P (0) = 1 $$$$

Lean4

@[simp]
theorem constVAdd_zero : constVAdd P (0 : G) = 1 :=
  ext <| zero_vadd G

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