Documentation Verification Report

OfFieldLabel

📁 Source: PhysLean/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfFieldLabel.lean

Statistics

Metric	Count
Definitions `ofFieldLabel`	1
Theorems `ext_ofFieldLabel`, `mem_ofFieldLabel_fiveHd`, `mem_ofFieldLabel_fiveHu`, `mem_ofFieldLabel_fiveMatter`, `ofFieldLabel_empty`, `ofFieldLabel_mono`	6
Total	7

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`ofFieldLabel` 📖	CompOp	6 math math: `mem_ofFieldLabel_fiveHu`, `mem_ofFieldLabel_fiveMatter`, `mem_ofFieldLabel_fiveHd`, `ofFieldLabel_empty`, `map_ofFieldLabel`, `ofFieldLabel_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_ofFieldLabel` 📖	—	`ofFieldLabel`	—	—	—
`mem_ofFieldLabel_fiveHd` 📖	mathematical	—	`ofFieldLabel` `SuperSymmetry.SU5.FieldLabel.fiveHd` `SuperSymmetry.SU5.FieldLabel.fiveBarHd`	—	—
`mem_ofFieldLabel_fiveHu` 📖	mathematical	—	`ofFieldLabel` `SuperSymmetry.SU5.FieldLabel.fiveHu` `SuperSymmetry.SU5.FieldLabel.fiveBarHu`	—	—
`mem_ofFieldLabel_fiveMatter` 📖	mathematical	—	`ofFieldLabel` `SuperSymmetry.SU5.FieldLabel.fiveMatter` `SuperSymmetry.SU5.FieldLabel.fiveBarMatter`	—	—
`ofFieldLabel_empty` 📖	mathematical	—	`ofFieldLabel` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`ofFieldLabel_mono` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`ofFieldLabel`	—	`subset_def`

---

← Back to Index