Theorems · Theorem · linear algebra

Module.dualProdDualEquivDual_apply_apply

∀ (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'] (f : (M →ₗ[R] R) × (M' →ₗ[R] R)) (a : M × M'),
  ((Module.dualProdDualEquivDual R M M') f) a = f.1 a.1 + f.2 a.2

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule