liftOn_mk'

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Localization.liftOn_mk'

← MathLib Explorer

English

A simp lemma for liftOn' on the mk' construction, showing evaluation is preserved.

Русский

Лемма simp для liftOn' на mk' сохраняет вычисление.

LaTeX

$$$\text{liftOn'} ( (\mathrm{monoidOf} S).mk' a b ) f H = f a b$$$

Lean4

@[to_additive (attr := simp)]
theorem liftOn_mk' {p : Sort u} (f : M → S → p) (H) (a : M) (b : S) : liftOn ((monoidOf S).mk' a b) f H = f a b := by
  rw [← mk_eq_monoidOf_mk', liftOn_mk]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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