Theorems · Definition · linear algebra

Module.dualProdDualEquivDual

(R : Type u_1) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (M' : Type u_4) →
            [inst_3 : AddCommMonoid M'] →
              [inst_4 : Module R M'] → (Module.Dual R M × Module.Dual R M') ≃ₗ[R] Module.Dual R (M × M')

Taking duals distributes over products.

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule