Structures · Algebra
RootPairing.IsNotG2
A prop-valued typeclass stating that a crystallographic, reduced, irreducible root system is not
𝔤₂.
- Shape
- One type argument · adds pairingIn_mem_zero_one_two
Extends3
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 by9
- RootPairing.chainBotCoeff_add_chainTopCoeff_le_two
- RootPairing.chainBotCoeff_if_one_zero
- RootPairing.IsNotG2.pairingIn_mem_zero_one_two
- RootPairing.pairingIn_le_zero_of_root_add_mem
- RootPairing.chainTopCoeff_if_one_zero
- RootPairing.zero_le_pairingIn_of_root_sub_mem
- RootPairing.IsNotG2.toIsReduced
- RootPairing.IsNotG2.toIsValuedIn
- RootPairing.IsNotG2.toIsIrreducible