Theorems · Theorem · nonassociative algebras

RootPairing.IsG2.exists_pairingIn_neg_three

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.IsG2],
  ∃ i j, P.pairingIn ℤ i j = -3

Defined in: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Cited by: 3 results in Mathlib
Foundations: Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RootPairing.IsG2

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
RootPairingstatement and proof · cited by 710
RootPairing.pairingInstatement · cited by 100
RootPairing.IsG2statement and proof · cited by 8

Cited by4

Results whose statement or proof uses this declaration.

RootPairing.IsG2.nonemptyproof · cited by 1
RootPairing.IsG2.pairingIn_mem_zero_one_threeproof · cited by 1
RootPairing.IsG2.toEmbeddedG2proof · cited by 1
RootPairing.isG2_iffproof · cited by 0