normalize_out — Mathlib

English

For any a in Associates α, applying normalize to out(a) yields out(a) again: normalize(out(a)) = out(a).

Русский

Для любого a ∈ Associates α применение normalize к out(a) даёт то же самое: normalize(out(a)) = out(a).

LaTeX

$$$$ \\operatorname{normalize}(\\operatorname{out}(a)) = \\operatorname{out}(a) $$$$

Lean4

@[simp]
theorem normalize_out (a : Associates α) : normalize a.out = a.out :=
  Quotient.inductionOn a normalize_idem

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