mk_get

Mathlib.Data.QPF.Multivariate.Constructions.Const

URI: https://scilib.ai/kg/mathlib#MvQPF.Const.mk_get

English

The composition mk followed by get is the identity on A, i.e., mk(get(z)) = z for z in Const.

Русский

Сжатие mk за которым следует get даёт тождество на A: mk(get(z)) = z.

LaTeX

$$$\mathrm{Const.mk}(\mathrm{Const.get}(z)) = z,$$$

Lean4

@[simp]
protected theorem mk_get (x : Const n A α) : Const.mk (Const.get x) = x :=
  rfl

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

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

Разделы

Аффилиация

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