coe_singletonMulHom — Mathlib

English

The coercion of the singleton homomorphism equals the canonical singleton function.

Русский

Сведение к функции-одиночке сопоставляется с канонической функцией одиночного множества.

LaTeX

$$Eq (MulHom.funLike.coe Finset.singletonMulHom) Finset.instSingleton.singleton$$

Lean4

@[to_additive (attr := simp)]
theorem coe_singletonMulHom : (singletonMulHom : α → Finset α) = singleton :=
  rfl

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