mk_div

Mathlib.GroupTheory.QuotientGroup.Defs

URI: https://scilib.ai/kg/mathlib#QuotientGroup.mk_div

English

The subgroup defined by a congruence c on a group G consists of all elements x with c(x,1) holds.

Русский

Подгруппа, определяемая конгруэнсией c на группе G, состоит из элементов x, для которых c(x,1) верно.

LaTeX

$$Con.subgroup c = { x ∈ G | c x 1 }$$

Lean4

@[to_additive (attr := simp)]
theorem mk_div (a b : G) : ((a / b : G) :  Q ) = a / b :=
  rfl

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

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

Разделы

Аффилиация

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