instCanLift

Mathlib.Algebra.Group.WithOne.Defs

URI: https://scilib.ai/kg/mathlib#WithOne.instCanLift

English

There is a CanLift instance lifting from α to WithOne α with the predicate a ≠ 1.

Русский

Существует экземпляр CanLift, переводящий элементы α в WithOne α с условием a ≠ 1.

LaTeX

$$$\text{CanLift} \ (\mathrm{WithOne}\ α)\ α\ WithOne.coe \ (\lambda a. a \neq 1)$$$

Lean4

@[to_additive]
instance instCanLift : CanLift (WithOne α) α (↑) fun a => a ≠ 1 where prf _ := ne_one_iff_exists.1

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

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

Разделы

Аффилиация

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