Theorems · Definition · commutative algebra

LinearEquiv.piUnique

{α : Type u_9} →
  [inst : Unique α] →
    (R : Type u_10) →
      [inst_1 : Semiring R] →
        (f : α → Type u_11) →
          [inst_2 : (x : α) → AddCommMonoid (f x)] →
            [inst_3 : (x : α) → Module R (f x)] → ((t : α) → f t) ≃ₗ[R] f default

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.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniqueSemiringAddCommMonoidModule