instNonemptyNormalizationMonoid — Mathlib

English

There exists a normalization monoid structure on α, i.e., there is at least one NormalizationMonoid structure on α.

Русский

Существует структура нормализации моноида на α, то есть существует хотя бы одна структура NormalizationMonoid(α).

LaTeX

$$$$ \\exists \\mathcal{N} : \\text{NormalizationMonoid}(\\alpha). $$$$

Lean4

instance [NormalizationMonoid α] : Nonempty (NormalizationMonoid α) :=
  ⟨‹_›⟩

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