instFunLike

Mathlib.GroupTheory.GroupExtension.Defs

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

English

Details of the transitive property of equivalences between extensions (auxiliary lemma).

Русский

Детали свойств перехода эквивалентностей между расширениями (вспомогательный лемма).

LaTeX

$$$\\text{Equiv.trans}_{eq_1}$$$

Lean4

@[to_additive]
instance : FunLike S.Section G E where
  coe := toFun
  coe_injective' := fun ⟨_, _⟩ ⟨_, _⟩ _ ↦ by congr

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

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

Разделы

Аффилиация

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