Theorems · Definition · linear algebra

IsBaseChange.toDual

{R : Type u_1} →
  [inst : CommSemiring R] →
    {V : Type u_2} →
      [inst_1 : AddCommMonoid V] →
        [inst_2 : Module R V] →
          {W : Type u_3} →
            [inst_3 : AddCommMonoid W] →
              [inst_4 : Module R W] →
                {A : Type u_4} →
                  [inst_5 : CommSemiring A] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Module A W] →
                        [inst_8 : IsScalarTower R A W] →
                          {j : V →ₗ[R] W} → IsBaseChange A j → Module.Dual R V →ₗ[R] Module.Dual A W

The base change of an element of the dual.

Defined in

Mathlib.LinearAlgebra.Dual.BaseChange

Cited by

6 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleCommSemiringAlgebraModuleIsScalarTower