out_one — Mathlib

English

Let α be a CancelCommMonoidWithZero and a NormalizationMonoid. The representative map from the associates to α sends the unit to the unit: out(1) = 1.

Русский

Пусть α имеет CancelCommMonoidWithZero и NormalizationMonoid. Отображение представителя из множества ассоциированных элементов в α отправляет единицу в единицу: out(1) = 1.

LaTeX

$$$$ \\operatorname{out}(1) = 1 $$$$

Lean4

@[simp]
theorem out_one : (1 : Associates α).out = 1 :=
  normalize_one

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