Theorems · Definition · linear algebra

LinearEquiv.funUnique

(ι : Type u_5) →
  (R : Type u_6) →
    (M : Type u_7) →
      [Unique ι] → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (ι → M) ≃ₗ[R] M

If ι has a unique element, then ι → M is linearly equivalent to M.

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

7 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

UniqueSemiringAddCommMonoidModule