Theorems · Definition · nonassociative algebras

RootPairing.chainTopIdx

{ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [Finite ι] →
          [inst : CommRing R] →
            [CharZero R] →
              [IsDomain R] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : AddCommGroup N] →
                      [inst_6 : Module R N] → {P : RootPairing ι R M N} → [P.IsCrystallographic] → ι → ι → ι

If α = P.root i and β = P.root j are linearly independent, this is the index of the root β + p • α where β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β. In the absence of linear independence, it takes a junk value.

Defined in

Mathlib.LinearAlgebra.RootSystem.Chain

Cited by

8 results in Mathlib

Foundations

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

Assumes

FiniteCommRingCharZeroIsDomainAddCommGroupModuleAddCommGroupModuleRootPairing.IsCrystallographic