Documentation

PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps

Family Maps for SM with RHN #

We give some properties of the family maps for the SM with RHN, in particular, we define family universal maps in the case of LinSols, QuadSols, and Sols.

source
def SMRHN.PlusU1.familyUniversalLinear (n : ℕ) :
(PlusU1 1).LinSols →ₗ[ℚ] (PlusU1 n).LinSols

The family universal maps on LinSols.

Equations
    Instances For
      source
      def SMRHN.PlusU1.familyUniversalQuad (n : ℕ) :
      (PlusU1 1).QuadSols → (PlusU1 n).QuadSols

      The family universal maps on QuadSols.

      Equations
        Instances For
          source
          def SMRHN.PlusU1.familyUniversalAF (n : ℕ) :
          (PlusU1 1).Sols → (PlusU1 n).Sols

          The family universal maps on Sols.

          Equations
            Instances For