Theorems · Definition · nonassociative algebras
RootPairing.Base.equivOfCartanMatrixEq
{ι : 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] →
[CharZero R] →
[IsDomain R] →
[Finite ι] →
{ι₂ : Type u_6} →
{M₂ : Type u_7} →
{N₂ : Type u_8} →
[inst_8 : AddCommGroup M₂] →
[inst_9 : Module R M₂] →
[inst_10 : AddCommGroup N₂] →
[inst_11 : Module R N₂] →
{P : RootPairing ι R M N} →
[P.IsRootSystem] →
[inst_13 : P.IsCrystallographic] →
[P.IsReduced] →
(b : P.Base) →
{P₂ : RootPairing ι₂ R M₂ N₂} →
[inst_15 : P₂.IsCrystallographic] →
(b₂ : P₂.Base) →
(e : ↥b.support ≃ ↥b₂.support) →
[Finite ι₂] →
[P₂.IsRootSystem] →
[P₂.IsReduced] →
(∀ (i j : ↥b.support),
b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j) →
P.Equiv P₂A root system is determined by its Cartan matrix.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites33
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idproof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- Finsetstatement · cited by 13,712
- AddCommGroupstatement and proof · cited by 12,871
- Equivstatement and proof · cited by 8,337
- Fintypeproof · cited by 7,736
- Set.rangeproof · cited by 4,705
- Equiv.symmproof · cited by 3,681
- LinearEquivproof · cited by 3,317
- Finitestatement and proof · cited by 3,029
Cited by1
Results whose statement or proof uses this declaration.
- RootPairing.GeckConstruction.equivRootSystemproof · cited by 0