Documentation Verification Report

Modules

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/Weyl/Modules.lean

Statistics

Metric	Count
Definitions `AltLeftHandedModule`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleComplex`, `toFin2ℂ`, `toFin2ℂEquiv`, `toFin2ℂFun`, `val`, `AltRightHandedModule`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleComplex`, `toFin2ℂ`, `toFin2ℂEquiv`, `toFin2ℂFun`, `val`, `LeftHandedModule`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleComplex`, `toFin2ℂ`, `toFin2ℂEquiv`, `toFin2ℂFun`, `val`, `RightHandedModule`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleComplex`, `toFin2ℂ`, `toFin2ℂEquiv`, `toFin2ℂFun`, `val`	32
Theorems `toFin2ℂEquiv_apply`, `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`, `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`, `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`, `toFin2ℂEquiv_symm_apply_val`	8
Total	40

Fermion

Definitions

Name	Category	Theorems
`AltLeftHandedModule` 📖	CompData	4 math math: `AltLeftHandedModule.toFin2ℂEquiv_apply`, `AltLeftHandedModule.toFin2ℂEquiv_symm_apply_val`, `leftHandedAltEquiv_hom_hom_apply`, `leftHandedToAlt_hom_apply`
`AltRightHandedModule` 📖	CompData	2 math math: `AltRightHandedModule.toFin2ℂEquiv_symm_apply_val`, `AltRightHandedModule.toFin2ℂEquiv_apply`
`LeftHandedModule` 📖	CompData	4 math math: `LeftHandedModule.toFin2ℂEquiv_apply`, `leftHandedAltEquiv_inv_hom_apply`, `LeftHandedModule.toFin2ℂEquiv_symm_apply_val`, `leftHandedAltTo_hom_apply`
`RightHandedModule` 📖	CompData	2 math math: `RightHandedModule.toFin2ℂEquiv_symm_apply_val`, `RightHandedModule.toFin2ℂEquiv_apply`

Fermion.AltLeftHandedModule

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	4 math math: `toFin2ℂEquiv_apply`, `toFin2ℂEquiv_symm_apply_val`, `Fermion.leftHandedAltEquiv_hom_hom_apply`, `Fermion.leftHandedToAlt_hom_apply`
`instModuleComplex` 📖	CompOp	4 math math: `toFin2ℂEquiv_apply`, `toFin2ℂEquiv_symm_apply_val`, `Fermion.leftHandedAltEquiv_hom_hom_apply`, `Fermion.leftHandedToAlt_hom_apply`
`toFin2ℂ` 📖	CompOp	5 math math: `Fermion.altLeftBasis_toFin2ℂ`, `Fermion.altLeftContraction_hom_tmul`, `Fermion.leftHandedAltEquiv_inv_hom_apply`, `Fermion.leftAltContraction_hom_tmul`, `Fermion.leftHandedAltTo_hom_apply`
`toFin2ℂEquiv` 📖	CompOp	4 math math: `toFin2ℂEquiv_apply`, `toFin2ℂEquiv_symm_apply_val`, `Fermion.leftHandedAltEquiv_hom_hom_apply`, `Fermion.leftHandedToAlt_hom_apply`
`toFin2ℂFun` 📖	CompOp	1 math math: `toFin2ℂEquiv_apply`
`val` 📖	CompOp	1 math math: `toFin2ℂEquiv_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFin2ℂEquiv_apply` 📖	mathematical	—	`Fermion.AltLeftHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv` `toFin2ℂFun`	—	—
`toFin2ℂEquiv_symm_apply_val` 📖	mathematical	—	`val` `Fermion.AltLeftHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv`	—	—

Fermion.AltRightHandedModule

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	2 math math: `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`
`instModuleComplex` 📖	CompOp	2 math math: `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`
`toFin2ℂ` 📖	CompOp	3 math math: `Fermion.rightAltContraction_hom_tmul`, `Fermion.altRightBasis_toFin2ℂ`, `Fermion.altRightContraction_hom_tmul`
`toFin2ℂEquiv` 📖	CompOp	2 math math: `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`
`toFin2ℂFun` 📖	CompOp	1 math math: `toFin2ℂEquiv_apply`
`val` 📖	CompOp	1 math math: `toFin2ℂEquiv_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFin2ℂEquiv_apply` 📖	mathematical	—	`Fermion.AltRightHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv` `toFin2ℂFun`	—	—
`toFin2ℂEquiv_symm_apply_val` 📖	mathematical	—	`val` `Fermion.AltRightHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv`	—	—

Fermion.LeftHandedModule

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	4 math math: `toFin2ℂEquiv_apply`, `Fermion.leftHandedAltEquiv_inv_hom_apply`, `toFin2ℂEquiv_symm_apply_val`, `Fermion.leftHandedAltTo_hom_apply`
`instModuleComplex` 📖	CompOp	4 math math: `toFin2ℂEquiv_apply`, `Fermion.leftHandedAltEquiv_inv_hom_apply`, `toFin2ℂEquiv_symm_apply_val`, `Fermion.leftHandedAltTo_hom_apply`
`toFin2ℂ` 📖	CompOp	5 math math: `Fermion.altLeftContraction_hom_tmul`, `Fermion.leftHandedAltEquiv_hom_hom_apply`, `Fermion.leftAltContraction_hom_tmul`, `Fermion.leftHandedToAlt_hom_apply`, `Fermion.leftBasis_toFin2ℂ`
`toFin2ℂEquiv` 📖	CompOp	4 math math: `toFin2ℂEquiv_apply`, `Fermion.leftHandedAltEquiv_inv_hom_apply`, `toFin2ℂEquiv_symm_apply_val`, `Fermion.leftHandedAltTo_hom_apply`
`toFin2ℂFun` 📖	CompOp	1 math math: `toFin2ℂEquiv_apply`
`val` 📖	CompOp	1 math math: `toFin2ℂEquiv_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFin2ℂEquiv_apply` 📖	mathematical	—	`Fermion.LeftHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv` `toFin2ℂFun`	—	—
`toFin2ℂEquiv_symm_apply_val` 📖	mathematical	—	`val` `Fermion.LeftHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv`	—	—

Fermion.RightHandedModule

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	2 math math: `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`
`instModuleComplex` 📖	CompOp	2 math math: `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`
`toFin2ℂ` 📖	CompOp	3 math math: `Fermion.rightAltContraction_hom_tmul`, `Fermion.altRightContraction_hom_tmul`, `Fermion.rightBasis_toFin2ℂ`
`toFin2ℂEquiv` 📖	CompOp	2 math math: `toFin2ℂEquiv_symm_apply_val`, `toFin2ℂEquiv_apply`
`toFin2ℂFun` 📖	CompOp	1 math math: `toFin2ℂEquiv_apply`
`val` 📖	CompOp	1 math math: `toFin2ℂEquiv_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFin2ℂEquiv_apply` 📖	mathematical	—	`Fermion.RightHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv` `toFin2ℂFun`	—	—
`toFin2ℂEquiv_symm_apply_val` 📖	mathematical	—	`val` `Fermion.RightHandedModule` `instAddCommMonoid` `instModuleComplex` `toFin2ℂEquiv`	—	—

---

← Back to Index