Documentation Verification Report

Matrix

📁 Source: Mathlib/GroupTheory/Coxeter/Matrix.lean

Statistics

Metric	Count
Definitions `CoxeterMatrix`, `A`, `Aₙ`, `B`, `Bₙ`, `D`, `Dₙ`, `E₆`, `E₇`, `E₈`, `F₄`, `G₂`, `H₃`, `H₄`, `I`, `I₂ₙ`, `instCoeFunMatrixNat`, `reindex`	18
Theorems `diagonal`, `ext`, `ext_iff`, `isSymm`, `off_diagonal`, `reindex_apply`, `symmetric`	7
Total	25

CoxeterMatrix

Definitions

Name	Category	Theorems
`A` 📖	CompOp	—
`Aₙ` 📖	CompOp	—
`B` 📖	CompOp	—
`Bₙ` 📖	CompOp	—
`D` 📖	CompOp	—
`Dₙ` 📖	CompOp	—
`E₆` 📖	CompOp	—
`E₇` 📖	CompOp	—
`E₈` 📖	CompOp	—
`F₄` 📖	CompOp	—
`G₂` 📖	CompOp	—
`H₃` 📖	CompOp	—
`H₄` 📖	CompOp	—
`I` 📖	CompOp	—
`I₂ₙ` 📖	CompOp	—
`instCoeFunMatrixNat` 📖	CompOp	—
`reindex` 📖	CompOp	6 math math: `CoxeterSystem.reindex_mulEquiv`, `reindex_relationsSet`, `reindexGroupEquiv_apply_simple`, `reindex_apply`, `CoxeterSystem.reindex_simple`, `reindexGroupEquiv_symm_apply_simple`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonal` 📖	mathematical	—	`M`	—	—
`ext` 📖	—	`M`	—	—	—
`ext_iff` 📖	mathematical	—	`M`	—	`ext`
`isSymm` 📖	mathematical	—	`Matrix.IsSymm` `M`	—	—
`off_diagonal` 📖	—	—	—	—	—
`reindex_apply` 📖	mathematical	—	`M` `reindex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`symmetric` 📖	mathematical	—	`M`	—	`Matrix.IsSymm.apply` `isSymm`

(root)

Definitions

Name	Category	Theorems
`CoxeterMatrix` 📖	CompData	1 math math: `IsCoxeterGroup.nonempty_system`

---

← Back to Index