coe_pureMonoidHom — Mathlib

English

The coercion of pureMonoidHom equals the pure operation, i.e., the underlying function is the same as the pure map.

Русский

Прямая сведение (коэрсия) pureMonoidHom совпадает с операцией чистого фильтра; внутреннее отображение задано совпадающе.

LaTeX

$$$(\text{pureMonoidHom} : \alpha \to \mathrm{Filter}(\alpha)) = \text{pure}.$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_pureMonoidHom : (pureMonoidHom : α → Filter α) = pure :=
  rfl

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