unique_one — Mathlib

English

In any type with a unique element and a multiplicative identity, the default element equals the identity.

Русский

В любом множестве, обладающем единственным элементом и единицей умножения, обозначение по умолчанию совпадает с единицей.

LaTeX

$$$\forall \alpha\; \big(\text{Unique}(\alpha) \wedge \text{One}(\alpha)\big) \Rightarrow \text{default}(\alpha) = 1_{\alpha}$$$

Lean4

@[to_additive]
theorem unique_one {α : Type*} [Unique α] [One α] : default = (1 : α) :=
  Unique.default_eq 1

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