quot_mk_eq_ι — Mathlib

English

The canonical quotient representative of an element m in X equals its image under the canonical embedding ι: X → FreeAlgebra R X.

Русский

Канонический представитель элемента m из X в виде элемента в FreeAlgebra R X через вложение ι совпадает с образцом m.

LaTeX

$$$\quot mk (FreeAlgebra.Rel\ R\ X)\ m = ι\ R\ m$$$

Lean4

@[simp]
theorem quot_mk_eq_ι (m : X) : Quot.mk (FreeAlgebra.Rel R X) m = ι R m := by rw [ι_def]

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