instCoeSubgroup

Mathlib.Topology.Algebra.Group.ClosedSubgroup

URI: https://scilib.ai/kg/mathlib#ClosedSubgroup.instCoeSubgroup

English

There is a canonical Coe between ClosedSubgroup G and Subgroup G.

Русский

Существует каноническое отображение-коe между ClosedSubgroup G и Subgroup G.

LaTeX

$$$ \\text{Coe}(ClosedSubgroup G) \\;=\\; Subgroup G $$$

Lean4

@[to_additive]
instance : Coe (ClosedSubgroup G) (Subgroup G) where coe := toSubgroup

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

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

Разделы

Аффилиация

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