English
The symm inverse of piFinTwo sends a pair (a,b) to the function x ↦ if x=0 then a else b.
Русский
Обратное к piFinTwo от пары (a,b) к функции x ↦ если x=0, то a, иначе b.
LaTeX
$$$$ (\\text{piFinTwo } R M)^{\\!\\mathrm{symm}} (a,b) = \\mathrm{fun}\\; x \\mapsto \\begin{cases} a, & x=0 \\\\ b, & x=1 \\end{cases}, $$$$
Lean4
/-- If `ι` has a unique element, then `ι → M` is linearly equivalent to `M`. -/
@[simps +simpRhs -fullyApplied symm_apply]
def funUnique (ι R M : Type*) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] : (ι → M) ≃ₗ[R] M :=
{ Equiv.funUnique ι M with
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl }
