coe_mk

Mathlib.GroupTheory.GroupExtension.Defs

URI: https://scilib.ai/kg/mathlib#GroupExtension.Section.coe_mk

English

The coercion of the constructor mk is the given σ.

Русский

Коэрцонка конструктора mk совпадает с заданной σ.

LaTeX

$$$(mk\\ \\sigma \\ h\\sigma : G \\to E) = \\sigma$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mk (σ : G → E) (hσ : Function.RightInverse σ S.rightHom) : (mk σ hσ : G → E) = σ :=
  rfl

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

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

Разделы

Аффилиация

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