English
If α has a unique element, then the product over α of a family of modules is canonically isomorphic to the module at the unique index: ∏_{t∈α} f(t) ≃ f(default).
Русский
Если у α имеется единственный элемент, то произведение по α семейства модулей естественным образом изоморфно модулю для единственного индекса: ∏ f(t) ≃ f(default).
LaTeX
$$$ \prod_{t:\alpha} f(t) \simeq f(\mathrm{default}) $$$
Lean4
/-- The product `Π t : α, f t` of a family of modules is linearly isomorphic to the module
`f ⬝` when `α` only contains `⬝`.
This is `Equiv.piUnique` as a `LinearEquiv`.
-/
@[simps -fullyApplied]
def piUnique {α : Type*} [Unique α] (R : Type*) [Semiring R] (f : α → Type*) [∀ x, AddCommMonoid (f x)]
[∀ x, Module R (f x)] : (Π t : α, f t) ≃ₗ[R] f default
where
__ := Equiv.piUnique _
map_add' _ _ := rfl
map_smul' _ _ := rfl
