congr_mk'

Mathlib.GroupTheory.QuotientGroup.Defs

URI: https://scilib.ai/kg/mathlib#QuotientGroup.congr_mk'

English

Variant of congr_mk using mk' for representatives; the result matches mk' on the image.

Русский

Вариант congr_mk с использованием mk' для представителей; результат совпадает с mk' на образе.

LaTeX

$$$\\text{congr } G' H' e (\\mathrm{mk}' G' x) = \\mathrm{mk}' H'(e x)$$$

Lean4

theorem congr_mk' (e : G ≃* H) (he : G'.map ↑e = H') (x) : congr G' H' e he (mk' G' x) = mk' H' (e x) :=
  rfl

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

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

Разделы

Аффилиация

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