subsingleton_iff — Mathlib

English

In an Additive torsor, the subsingleton property of the group G is equivalent to the subsingleton property of the torsor P.

Русский

В аддитивном торсоре свойство «множество содержит не более одного элемента» для группы G эквивалентно аналогичному свойству для торсора P.

LaTeX

$$Subsingleton(G) \iff Subsingleton(P)$$

Lean4

theorem subsingleton_iff (G P : Type*) [AddGroup G] [AddTorsor G P] : Subsingleton G ↔ Subsingleton P :=
  by
  inhabit P
  exact (Equiv.vaddConst default).subsingleton_congr

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