sumArrowEquivProdArrow — Mathlib

English

There is an algebra isomorphism between the function space on a disjoint sum α ⊕ β and the product of function spaces α → S and β → S.

Русский

Существует алгебраическое изоморфизм между множеством функций на раздельном суммарном индексе α ⊕ β и произведением множеств функций α → S и β → S.

LaTeX

$$$$ (\alpha \oplus \beta \to S) \cong_R (\alpha \to S) \times (\beta \to S). $$$$

Lean4

/-- `Equiv.sumArrowEquivProdArrow` as an algebra equivalence. -/
def sumArrowEquivProdArrow : (α ⊕ β → S) ≃ₐ[R] (α → S) × (β → S) :=
  .ofRingEquiv (f := .sumArrowEquivProdArrow α β S)
    (by intro; ext <;> simp)
      -- Priority `low` to ensure generic `map_{add, mul, zero, one}` lemmas are applied first

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