mk_quot_out — Mathlib

English

The representative from Quot.out of an associate class is associated to the original element.

Русский

Представитель из Quot.out класса ассоциированности ассоциирован с исходным элементом.

LaTeX

$$$$\mathrm{Quot.out}(\mathrm{Associates.mk} \ a) \sim_{\mathrm{a}} a.$$$$

Lean4

theorem mk_quot_out [Monoid M] (a : M) : Quot.out (Associates.mk a) ~ᵤ a := by
  rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]

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