Cartan

📁 Source: Mathlib/Data/Matrix/Cartan.lean

Statistics

Metric	Count
Definitions `A`, `B`, `C`, `D`, `E₆`, `E₇`, `E₈`, `F₄`, `G₂`, `instDecidablePredMatrixIntIsSimplyLacedOfFintypeOfDecidableEq`, `IsSimplyLaced`	11
Theorems `A_apply_le_zero_of_ne`, `A_diag`, `A_isSymm`, `A_one`, `A_three`, `A_transpose`, `A_two`, `B_diag`, `B_off_diag_nonpos`, `B_one`, `B_transpose`, `B_two`, `C_diag`, `C_off_diag_nonpos`, `C_one`, `C_transpose`, `C_two`, `D_diag`, `D_four`, `D_isSymm`, `D_off_diag_nonpos`, `D_one`, `D_three`, `D_three'`, `D_transpose`, `D_two`, `E₆_diag`, `E₆_isSymm`, `E₆_off_diag_nonpos`, `E₆_transpose`, `E₇_diag`, `E₇_isSymm`, `E₇_off_diag_nonpos`, `E₇_transpose`, `E₈_diag`, `E₈_isSymm`, `E₈_off_diag_nonpos`, `E₈_transpose`, `F₄_det`, `F₄_diag`, `F₄_off_diag_nonpos`, `G₂_det`, `G₂_diag`, `G₂_off_diag_nonpos`, `isSimplyLaced_A`, `isSimplyLaced_D`, `isSimplyLaced_E₆`, `isSimplyLaced_E₇`, `isSimplyLaced_E₈`, `not_isSimplyLaced_F₄`, `not_isSimplyLaced_G₂`, `isSimplyLaced_iff_of_linearOrder`, `isSimplyLaced_transpose`	53
Total	64

CartanMatrix

Definitions

Name	Category	Theorems
`A` 📖	CompOp	12 math math: `isSimplyLaced_A`, `D_three'`, `C_one`, `A_isSymm`, `A_three`, `A_apply_le_zero_of_ne`, `A_two`, `D_one`, `A_one`, `B_one`, `A_transpose`, `A_diag`
`B` 📖	CompOp	6 math math: `B_off_diag_nonpos`, `B_diag`, `C_transpose`, `B_two`, `B_transpose`, `B_one`
`C` 📖	CompOp	6 math math: `C_two`, `C_off_diag_nonpos`, `C_transpose`, `C_one`, `B_transpose`, `C_diag`
`D` 📖	CompOp	10 math math: `D_four`, `D_isSymm`, `isSimplyLaced_D`, `D_three`, `D_off_diag_nonpos`, `D_three'`, `D_transpose`, `D_two`, `D_one`, `D_diag`
`E₆` 📖	CompOp	5 math math: `E₆_transpose`, `E₆_diag`, `isSimplyLaced_E₆`, `E₆_off_diag_nonpos`, `E₆_isSymm`
`E₇` 📖	CompOp	5 math math: `isSimplyLaced_E₇`, `E₇_diag`, `E₇_isSymm`, `E₇_transpose`, `E₇_off_diag_nonpos`
`E₈` 📖	CompOp	5 math math: `E₈_off_diag_nonpos`, `E₈_isSymm`, `E₈_diag`, `isSimplyLaced_E₈`, `E₈_transpose`
`F₄` 📖	CompOp	4 math math: `not_isSimplyLaced_F₄`, `F₄_diag`, `F₄_off_diag_nonpos`, `F₄_det`
`G₂` 📖	CompOp	4 math math: `G₂_diag`, `G₂_det`, `not_isSimplyLaced_G₂`, `G₂_off_diag_nonpos`
`instDecidablePredMatrixIntIsSimplyLacedOfFintypeOfDecidableEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`A_apply_le_zero_of_ne` 📖	mathematical	—	`A`	—	—
`A_diag` 📖	mathematical	—	`Matrix.diag` `A` `Pi.instOfNat`	—	—
`A_isSymm` 📖	mathematical	—	`Matrix.IsSymm` `A`	—	`A_transpose`
`A_one` 📖	mathematical	—	`A` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`A_three` 📖	mathematical	—	`A` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`A_transpose` 📖	mathematical	—	`Matrix.transpose` `A`	—	`Matrix.ext`
`A_two` 📖	mathematical	—	`A` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`B_diag` 📖	mathematical	—	`B`	—	—
`B_off_diag_nonpos` 📖	mathematical	—	`B`	—	—
`B_one` 📖	mathematical	—	`B` `A`	—	—
`B_transpose` 📖	mathematical	—	`Matrix.transpose` `B` `C`	—	`Matrix.ext`
`B_two` 📖	mathematical	—	`B` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`C_diag` 📖	mathematical	—	`C`	—	—
`C_off_diag_nonpos` 📖	mathematical	—	`C`	—	—
`C_one` 📖	mathematical	—	`C` `A`	—	—
`C_transpose` 📖	mathematical	—	`Matrix.transpose` `C` `B`	—	`Matrix.transpose_transpose` `B_transpose`
`C_two` 📖	mathematical	—	`C` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`D_diag` 📖	mathematical	—	`D`	—	—
`D_four` 📖	mathematical	—	`D` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`D_isSymm` 📖	mathematical	—	`Matrix.IsSymm` `D`	—	`D_transpose`
`D_off_diag_nonpos` 📖	mathematical	—	`D`	—	—
`D_one` 📖	mathematical	—	`D` `A`	—	—
`D_three` 📖	mathematical	—	`D` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`D_three'` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.reindex` `Cycle.formPerm` `Cycle.ofList` `Cycle.Nodup` `Cycle.nodup_coe_iff` `D` `A`	—	`Cycle.nodup_coe_iff`
`D_transpose` 📖	mathematical	—	`Matrix.transpose` `D`	—	`Matrix.ext`
`D_two` 📖	mathematical	—	`D` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`E₆_diag` 📖	mathematical	—	`E₆`	—	`Fintype.complete`
`E₆_isSymm` 📖	mathematical	—	`Matrix.IsSymm` `E₆`	—	`E₆_transpose`
`E₆_off_diag_nonpos` 📖	mathematical	—	`E₆`	—	`Fintype.complete` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.instAddLeftMono` `Int.instZeroLEOneClass`
`E₆_transpose` 📖	mathematical	—	`Matrix.transpose` `E₆`	—	—
`E₇_diag` 📖	mathematical	—	`E₇`	—	`Fintype.complete`
`E₇_isSymm` 📖	mathematical	—	`Matrix.IsSymm` `E₇`	—	`E₇_transpose`
`E₇_off_diag_nonpos` 📖	mathematical	—	`E₇`	—	`Fintype.complete` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.instAddLeftMono` `Int.instZeroLEOneClass`
`E₇_transpose` 📖	mathematical	—	`Matrix.transpose` `E₇`	—	—
`E₈_diag` 📖	mathematical	—	`E₈`	—	`Fintype.complete`
`E₈_isSymm` 📖	mathematical	—	`Matrix.IsSymm` `E₈`	—	`E₈_transpose`
`E₈_off_diag_nonpos` 📖	mathematical	—	`E₈`	—	`Fintype.complete` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.instAddLeftMono` `Int.instZeroLEOneClass`
`E₈_transpose` 📖	mathematical	—	`Matrix.transpose` `E₈`	—	—
`F₄_det` 📖	mathematical	—	`Matrix.det` `Fin.fintype` `Int.instCommRing` `F₄`	—	—
`F₄_diag` 📖	mathematical	—	`F₄`	—	`Fintype.complete`
`F₄_off_diag_nonpos` 📖	mathematical	—	`F₄`	—	`Fintype.complete` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat`
`G₂_det` 📖	mathematical	—	`Matrix.det` `Fin.fintype` `Int.instCommRing` `G₂`	—	—
`G₂_diag` 📖	mathematical	—	`G₂`	—	`Fintype.complete`
`G₂_off_diag_nonpos` 📖	mathematical	—	`G₂`	—	`Fintype.complete` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.instAddLeftMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `Int.instZeroLEOneClass`
`isSimplyLaced_A` 📖	mathematical	—	`Matrix.IsSimplyLaced` `A`	—	—
`isSimplyLaced_D` 📖	mathematical	—	`Matrix.IsSimplyLaced` `D`	—	—
`isSimplyLaced_E₆` 📖	mathematical	—	`Matrix.IsSimplyLaced` `E₆`	—	`Matrix.isSimplyLaced_iff_of_linearOrder` `E₆_isSymm`
`isSimplyLaced_E₇` 📖	mathematical	—	`Matrix.IsSimplyLaced` `E₇`	—	`Matrix.isSimplyLaced_iff_of_linearOrder` `E₇_isSymm`
`isSimplyLaced_E₈` 📖	mathematical	—	`Matrix.IsSimplyLaced` `E₈`	—	`Matrix.isSimplyLaced_iff_of_linearOrder` `E₈_isSymm`
`not_isSimplyLaced_F₄` 📖	mathematical	—	`Matrix.IsSimplyLaced` `F₄`	—	—
`not_isSimplyLaced_G₂` 📖	mathematical	—	`Matrix.IsSimplyLaced` `G₂`	—	—

Matrix

Definitions

Name	Category	Theorems
`IsSimplyLaced` 📖	MathDef	9 math math: `CartanMatrix.isSimplyLaced_E₇`, `CartanMatrix.not_isSimplyLaced_F₄`, `CartanMatrix.isSimplyLaced_D`, `CartanMatrix.isSimplyLaced_A`, `isSimplyLaced_transpose`, `CartanMatrix.isSimplyLaced_E₆`, `CartanMatrix.isSimplyLaced_E₈`, `CartanMatrix.not_isSimplyLaced_G₂`, `isSimplyLaced_iff_of_linearOrder`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimplyLaced_iff_of_linearOrder` 📖	mathematical	`IsSymm`	`IsSimplyLaced`	—	`LT.lt.ne'` `Ne.lt_or_gt` `IsSymm.apply`
`isSimplyLaced_transpose` 📖	mathematical	—	`IsSimplyLaced` `transpose`	—	`IsSimplyLaced.eq_1` `Pairwise.eq_1`

---

← Back to Index