OAI/RepresentationTheory/FoulkesHowe/DualEquivalence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Problem346.symPowDualMap_isPerfPair line 14

    Source documentation

    The canonical symmetric-power pairing is perfect in finite dimension.

    instance symPowDualMap_isPerfPair : (symPowDualMap n V).IsPerfPair :=
…

    Mentions: OAI.Problem346.symPowDualMap

  2. def OAI.Problem346.symPowDualEquiv line 19

    Source documentation

    Symmetric powers commute with algebraic duality in finite dimension.

    def symPowDualEquiv :
    SymPow n (Module.Dual ℂ V) ≃ₗ[ℂ] Module.Dual ℂ (SymPow n V) :=
…

    Mentions: OAI.Problem346.SymPow

  3. theorem OAI.Problem346.symPowDualEquiv_toLinearMap line 23
  4. theorem OAI.Problem346.symPowDualEquiv_apply line 26
  5. theorem OAI.Problem346.symPowDualEquiv_monomial line 29