coe_of — Mathlib

English

The image of the generator a under the canonical embedding coincides with the corresponding generator in FreeCommRing.

Русский

образ генератора a через каноническое вложение совпадает с соответствующим генератором в FreeCommRing.

LaTeX

$$$\\uparrow(\\mathrm{FreeRing}.\\mathrm{of}(a)) = \\mathrm{FreeCommRing}.\\mathrm{of}(a)$$$

Lean4

@[simp]
protected theorem coe_of (a : α) : ↑(FreeRing.of a) = FreeCommRing.of a :=
  FreeRing.lift_of _ _

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