coeRingHom

Mathlib.RingTheory.FreeCommRing

URI: https://scilib.ai/kg/mathlib#FreeRing.coeRingHom

English

If x is supported on s, then map(↑) (restriction s x) = x.

Русский

Если опора x находится в s, то отображение map(↑) (restriction s x) совпадает с x.

LaTeX

$$$\\forall x\\, hxs: IsSupported(x, s),\\quad \\mathrm{map}(\\uparrow)(\\mathrm{restriction}(s)(x)) = x$$$

Lean4

/-- The natural map `FreeRing α → FreeCommRing α`, as a `RingHom`. -/
def coeRingHom : FreeRing α →+* FreeCommRing α :=
  toFreeCommRing

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru