pi

Mathlib.GroupTheory.Congruence.Basic

URI: https://scilib.ai/kg/mathlib#Con.pi

Lean4

/-- The product of an indexed collection of congruence relations. -/
@[to_additive /-- The product of an indexed collection of additive congruence relations. -/
    ]
def pi {ι : Type*} {f : ι → Type*} [∀ i, Mul (f i)] (C : ∀ i, Con (f i)) : Con (∀ i, f i) :=
  { @piSetoid _ _ fun i => (C i).toSetoid with mul' := fun h1 h2 i => (C i).mul (h1 i) (h2 i) }

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

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

Разделы

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

Аффилиация

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