instRing

Mathlib.Algebra.Ring.Shrink

URI: https://scilib.ai/kg/mathlib#Shrink.instRing

English

If α is a ring, then Shrink α is a ring (structure transported along the inverse of the shrink equivalence).

Русский

Если α — кольцо, то Shrink α является кольцом.

LaTeX

$$$(\text{Ring } \alpha) \Rightarrow \text{Ring}(\text{Shrink } \alpha)$$$

Lean4

instance [Ring α] : Ring (Shrink.{v} α) :=
  (equivShrink α).symm.ring

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

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

Разделы

Аффилиация

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