singletonMulHom_apply — Mathlib

English

The image of a singleton under the singletonMulHom is the singleton itself: singletonMulHom a = {a}.

Русский

Образ одноэлементного множества под singletonMulHom равен самому одноэлементному множеству: singletonMulHom a = {a}.

LaTeX

$$singletonMulHom_apply : (a : α) \\;: \\; singletonMulHom a = { a }$$

Lean4

@[to_additive (attr := simp)]
theorem singletonMulHom_apply (a : α) : singletonMulHom a = { a } :=
  rfl

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