exists_rep

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.exists_rep

English

Every element of Associates M has a representative in M.

Русский

Каждый элемент Associates(M) имеет представитель в M.

LaTeX

$$$ \forall a : \operatorname{Associates}(M), \exists a_0 : M, \operatorname{Associates.mk}(a_0) = a $$$

Lean4

theorem exists_rep [Monoid M] (a : Associates M) : ∃ a0 : M, Associates.mk a0 = a :=
  Quot.exists_rep a

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

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

Разделы

Аффилиация

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