Mathlib Map

Structures · Algebra

RootPairing.EmbeddedG2

A data-bearing typeclass which distinguishes a pair of roots whose pairing is -3. This is a sufficient condition for the span of this pair of roots to be a 𝔤₂ root system.

Defined in
Mathlib.LinearAlgebra.RootSystem.Finite.G2
Shape
One type argument · adds long, short, pairingIn_long_short

Extends2

Extended by0

Nothing extends this class yet.

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by52

Ancestors2