ndrec_mk

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Localization.ndrec_mk

← MathLib Explorer

English

The congruence r is equivalent to the Ore-style congruence oreEqv.

Русский

Конгруэнция r эквивалентна конгруэнции oreEqv в стиле Ore.

LaTeX

$$$ r S x y \iff (OreLocalization.oreEqv S M).r x y $$$

Lean4

@[to_additive (attr := simp)]
theorem ndrec_mk {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b)) (H) (a : M) (b : S) :
    (rec f H (mk a b) : p (mk a b)) = f a b :=
  rfl

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

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

Разделы

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

Аффилиация

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