funUnique — Mathlib

English

If the index type ι has a unique element, then the function space ι → S is isomorphic to S as an algebra over R.

Русский

Если множество индексов ι является уникальным, то пространство функций ι → S изоморфно S как алгебра над R.

LaTeX

$$$$ (\iota \to S) \simeq_R S \quad (\text{when } ι \text{ is unique}). $$$$

Lean4

/-- If `ι` has a unique element, then `ι → S` is isomorphic to `S` as an `R`-algebra. -/
def funUnique [Unique ι] : (ι → S) ≃ₐ[R] S :=
  .ofRingEquiv (f := .piUnique (fun i : ι ↦ S))
    (by simp)
      -- Priority `low` to ensure generic `map_{add, mul, zero, one}` lemmas are applied first

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