Documentation Verification Report

Basic

📁 Source: PhysLean/Mathematics/SO3/Basic.lean

Statistics

Metric	Count
Definitions `SO3`, `toEnd`, `toGL`, `toProd`, `SO3Group`, `SO3_notation`, `instTopologicalSpaceSO3`	7
Theorems `coe_inv`, `det_id_minus`, `det_minus_id`, `exists_basis_preserved`, `exists_stationary_vec`, `instIsTopologicalGroup`, `one_in_spectrum`, `one_is_eigenvalue`, `subtype_val_eq_toGL`, `toEnd_apply_ofLp`, `toGL_embedding`, `toGL_injective`, `toProd_apply`, `toProd_continuous`, `toProd_embedding`, `toProd_eq_transpose`, `toProd_injective`, `SO3Group_div`, `SO3Group_inv`, `SO3Group_mul_coe`, `SO3Group_one_coe`	21
Total	28

GroupTheory

Definitions

Name	Category	Theorems
`SO3` 📖	CompOp	14 math math: `SO3Group_div`, `SO3.toProd_continuous`, `SO3.toProd_eq_transpose`, `SO3Group_inv`, `SO3.instIsTopologicalGroup`, `SO3.toProd_injective`, `SO3.toProd_embedding`, `SO3.toGL_embedding`, `SO3Group_mul_coe`, `SO3.toProd_apply`, `SO3.subtype_val_eq_toGL`, `SO3.coe_inv`, `SO3.toGL_injective`, `SO3Group_one_coe`
`SO3Group` 📖	CompOp	14 math math: `SO3Group_div`, `SO3.toProd_continuous`, `SO3.toProd_eq_transpose`, `SO3Group_inv`, `SO3.instIsTopologicalGroup`, `SO3.toProd_injective`, `SO3.toProd_embedding`, `SO3.toGL_embedding`, `SO3Group_mul_coe`, `SO3.toProd_apply`, `SO3.subtype_val_eq_toGL`, `SO3.coe_inv`, `SO3.toGL_injective`, `SO3Group_one_coe`
`SO3_notation` 📖	CompOp	—
`instTopologicalSpaceSO3` 📖	CompOp	4 math math: `SO3.toProd_continuous`, `SO3.instIsTopologicalGroup`, `SO3.toProd_embedding`, `SO3.toGL_embedding`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SO3Group_div` 📖	mathematical	—	`SO3` `SO3Group`	—	—
`SO3Group_inv` 📖	mathematical	—	`SO3` `SO3Group`	—	—
`SO3Group_mul_coe` 📖	mathematical	—	`SO3` `SO3Group`	—	—
`SO3Group_one_coe` 📖	mathematical	—	`SO3` `SO3Group`	—	—

GroupTheory.SO3

Definitions

Name	Category	Theorems
`toEnd` 📖	CompOp	4 math math: `exists_stationary_vec`, `toEnd_apply_ofLp`, `exists_basis_preserved`, `one_is_eigenvalue`
`toGL` 📖	CompOp	4 math math: `toGL_embedding`, `toProd_apply`, `subtype_val_eq_toGL`, `toGL_injective`
`toProd` 📖	CompOp	5 math math: `toProd_continuous`, `toProd_eq_transpose`, `toProd_injective`, `toProd_embedding`, `toProd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inv` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.SO3Group`	—	—
`det_id_minus` 📖	—	—	—	—	`det_minus_id`
`det_minus_id` 📖	—	—	—	—	—
`exists_basis_preserved` 📖	mathematical	—	`toEnd`	—	`exists_stationary_vec`
`exists_stationary_vec` 📖	mathematical	—	`toEnd`	—	`one_is_eigenvalue`
`instIsTopologicalGroup` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.instTopologicalSpaceSO3` `GroupTheory.SO3Group`	—	`toGL_embedding`
`one_in_spectrum` 📖	—	—	—	—	`det_id_minus`
`one_is_eigenvalue` 📖	mathematical	—	`toEnd`	—	`one_in_spectrum`
`subtype_val_eq_toGL` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.SO3Group` `toGL`	—	—
`toEnd_apply_ofLp` 📖	mathematical	—	`toEnd`	—	—
`toGL_embedding` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.instTopologicalSpaceSO3` `GroupTheory.SO3Group` `toGL`	—	`toProd_embedding` `toGL_injective`
`toGL_injective` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.SO3Group` `toGL`	—	—
`toProd_apply` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.SO3Group` `toProd` `toGL`	—	—
`toProd_continuous` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.instTopologicalSpaceSO3` `GroupTheory.SO3Group` `toProd`	—	—
`toProd_embedding` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.instTopologicalSpaceSO3` `GroupTheory.SO3Group` `toProd`	—	`toProd_continuous` `toProd_injective`
`toProd_eq_transpose` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.SO3Group` `toProd`	—	—
`toProd_injective` 📖	mathematical	—	`GroupTheory.SO3` `GroupTheory.SO3Group` `toProd`	—	`toProd_eq_transpose`

---

← Back to Index