OAI/RepresentationTheory/FoulkesHowe/DegreeOne.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem346.symmetricAlgebra_ι_injective line 11
  2. lemma OAI.Problem346.symMonomialRaw_one line 20
  3. lemma OAI.Problem346.symPowSubmodule_one line 24
  4. def OAI.Problem346.symPowOneIntro line 38

    Source documentation

    The canonical inclusion of a vector into the degree-one symmetric power.

    def symPowOneIntro : V →ₗ[ℂ] SymPow 1 V :=
…

    Mentions: OAI.Problem346.SymPow

  5. lemma OAI.Problem346.symPowOneIntro_coe line 44
  6. lemma OAI.Problem346.symPowOneIntro_bijective line 47
  7. def OAI.Problem346.symPowOneEquiv line 60

    Source documentation

    The degree-one symmetric power is canonically the original vector space.

    def symPowOneEquiv : SymPow 1 V ≃ₗ[ℂ] V :=
…

    Mentions: OAI.Problem346.SymPow

  8. lemma OAI.Problem346.symPowOneEquiv_symm_apply line 63
  9. lemma OAI.Problem346.symPowOneEquiv_symMonomial line 68