kerLift_mk'

Mathlib.GroupTheory.QuotientGroup.Basic

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

English

The simp version of kerLift_mk: kerLift φ (mk g) = φ g.

Русский

Упрощённая версия kerLift_mk': kerLift φ (mk g) = φ g.

LaTeX

$$$(\\kerLift φ)(\\mathrm{mk}\\ g) = φ(g)$$$

Lean4

@[to_additive (attr := simp)]
theorem kerLift_mk' (g : G) : (kerLift φ) (mk g) = φ g :=
  lift_mk' _ _ _

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

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

Разделы

Аффилиация

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