Theorems · Definition · nonassociative algebras

RootPairing.RootPositiveForm.noConfusionType

Sort u →
  {ι : Type u_1} →
    {R : Type u_2} →
      {S : Type u_3} →
        {M : Type u_4} →
          {N : Type u_5} →
            [inst : CommRing S] →
              [inst_1 : LinearOrder S] →
                [inst_2 : CommRing R] →
                  [inst_3 : Algebra S R] →
                    [inst_4 : AddCommGroup M] →
                      [inst_5 : Module R M] →
                        [inst_6 : AddCommGroup N] →
                          [inst_7 : Module R N] →
                            {P : RootPairing ι R M N} →
                              [inst_8 : P.IsValuedIn S] →
                                RootPairing.RootPositiveForm S P →
                                  {ι' : Type u_1} →
                                    {R' : Type u_2} →
                                      {S' : Type u_3} →
                                        {M' : Type u_4} →
                                          {N' : Type u_5} →
                                            [inst' : CommRing S'] →
                                              [inst'_1 : LinearOrder S'] →
                                                [inst'_2 : CommRing R'] →
                                                  [inst'_3 : Algebra S' R'] →
                                                    [inst'_4 : AddCommGroup M'] →
                                                      [inst'_5 : Module R' M'] →
                                                        [inst'_6 : AddCommGroup N'] →
                                                          [inst'_7 : Module R' N'] →
                                                            {P' : RootPairing ι' R' M' N'} →
                                                              [inst'_8 : P'.IsValuedIn S'] →
                                                                RootPairing.RootPositiveForm S' P' → Sort u

Defined in

Mathlib.LinearAlgebra.RootSystem.RootPositive

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLinearOrderCommRingAlgebraAddCommGroupModuleAddCommGroupModuleRootPairing.IsValuedInCommRingLinearOrderCommRingAlgebraAddCommGroupModuleAddCommGroupModuleRootPairing.IsValuedIn