toPi

Mathlib.Algebra.Algebra.Spectrum.Pi

URI: https://scilib.ai/kg/mathlib#PreQuasiregular.toPi

Lean4

/-- The equivalence between pre-quasiregular elements of an indexed product and the indexed product
of pre-quasiregular elements. -/
def toPi [∀ i, NonUnitalSemiring (κ i)] : PreQuasiregular (∀ i, κ i) ≃* ∀ i, PreQuasiregular (κ i)
    where
  toFun := fun x i => .mk <| x.val i
  invFun := fun x => .mk <| fun i => (x i).val
  map_mul' _ _ := rfl

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

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

Разделы

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

Аффилиация

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