Documentation Verification Report

Submodule

📁 Source: PhysLean/Mathematics/InnerProductSpace/Submodule.lean

Statistics

Metric	Count
Definitions `submoduleToLp`	1
Theorems `mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal`, `mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal`, `mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal`, `mem_submodule_closure_iff_mem_submoduleToLp_closure`, `mem_submodule_iff_mem_submoduleToLp`, `submoduleToLp_closure`	6
Total	7

InnerProductSpaceSubmodule

Definitions

Name	Category	Theorems
`submoduleToLp` 📖	CompOp	6 math math: `mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal`, `mem_submodule_closure_iff_mem_submoduleToLp_closure`, `mem_submodule_iff_mem_submoduleToLp`, `submoduleToLp_closure`, `mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal`, `mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal` 📖	mathematical	—	`submoduleToLp`	—	`mem_submodule_iff_mem_submoduleToLp`
`mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal` 📖	mathematical	—	`submoduleToLp`	—	`mem_submodule_iff_mem_submoduleToLp`
`mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal` 📖	mathematical	—	`submoduleToLp`	—	`mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal` `submoduleToLp_closure`
`mem_submodule_closure_iff_mem_submoduleToLp_closure` 📖	mathematical	—	`submoduleToLp`	—	`submoduleToLp_closure`
`mem_submodule_iff_mem_submoduleToLp` 📖	mathematical	—	`submoduleToLp`	—	—
`submoduleToLp_closure` 📖	mathematical	—	`submoduleToLp`	—	`mem_submodule_iff_mem_submoduleToLp`

---

← Back to Index