get_mk

Mathlib.Data.QPF.Multivariate.Constructions.Const

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

English

The other inverse: for a value a ∈ A, get(mk(a)) = a.

Русский

Противоположная обратная связка: get(mk(a)) = a.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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