Documentation Verification Report

OfPotentialTerm

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

Statistics

Metric	Count
Definitions `ofPotentialTerm`, `ofPotentialTerm'`	2
Theorems `mem_ofPotentialTerm_iff_mem_ofPotentialTerm`, `ofPotentialTerm'_K2_finset`, `ofPotentialTerm'_W2_finset`, `ofPotentialTerm'_W3_finset`, `ofPotentialTerm'_W4_finset`, `ofPotentialTerm'_bottomYukawa_finset`, `ofPotentialTerm'_empty`, `ofPotentialTerm'_mono`, `ofPotentialTerm'_subset_ofPotentialTerm`, `ofPotentialTerm'_topYukawa_finset`, `ofPotentialTerm'_β_finset`, `ofPotentialTerm'_μ_finset`, `ofPotentialTerm_empty`, `ofPotentialTerm_mono`, `ofPotentialTerm_subset_ofPotentialTerm'`	15
Total	17

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`ofPotentialTerm` 📖	CompOp	7 math math: `ofPotentialTerm_subset_ofPotentialTerm'`, `mem_ofPotentialTerm_iff_mem_ofPotentialTerm`, `map_ofPotentialTerm_toFinset`, `ofPotentialTerm'_subset_ofPotentialTerm`, `ofPotentialTerm_mono`, `ofPotentialTerm_empty`, `mem_map_ofPotentialTerm_iff`
`ofPotentialTerm'` 📖	CompOp	16 math math: `ofPotentialTerm_subset_ofPotentialTerm'`, `mem_ofPotentialTerm_iff_mem_ofPotentialTerm`, `ofPotentialTerm'_mono`, `map_ofPotentialTerm'_toFinset`, `ofPotentialTerm'_W4_finset`, `ofPotentialTerm'_subset_ofPotentialTerm`, `ofPotentialTerm'_topYukawa_finset`, `ofPotentialTerm'_β_finset`, `allowsTerm_iff_zero_mem_ofPotentialTerm'`, `mem_map_ofPotentialTerm'_iff`, `ofPotentialTerm'_empty`, `ofPotentialTerm'_W2_finset`, `ofPotentialTerm'_W3_finset`, `ofPotentialTerm'_μ_finset`, `ofPotentialTerm'_bottomYukawa_finset`, `ofPotentialTerm'_K2_finset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_ofPotentialTerm_iff_mem_ofPotentialTerm` 📖	mathematical	—	`ofPotentialTerm` `ofPotentialTerm'`	—	`ofPotentialTerm_subset_ofPotentialTerm'` `ofPotentialTerm'_subset_ofPotentialTerm`
`ofPotentialTerm'_K2_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.K2` `qHd` `qHu` `Q10`	—	—
`ofPotentialTerm'_W2_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.W2` `qHd` `Q10`	—	—
`ofPotentialTerm'_W3_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.W3` `qHu` `Q5`	—	—
`ofPotentialTerm'_W4_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.W4` `qHd` `qHu` `Q5`	—	—
`ofPotentialTerm'_bottomYukawa_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.bottomYukawa` `qHd` `Q5` `Q10`	—	—
`ofPotentialTerm'_empty` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	`empty_Q5` `empty_Q10`
`ofPotentialTerm'_mono` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`ofPotentialTerm'`	—	`mem_ofPotentialTerm_iff_mem_ofPotentialTerm` `ofPotentialTerm_mono`
`ofPotentialTerm'_subset_ofPotentialTerm` 📖	mathematical	—	`ofPotentialTerm'` `ofPotentialTerm`	—	`ofPotentialTerm'_μ_finset` `ofPotentialTerm_mono` `subset_def` `ofPotentialTerm'_β_finset` `ofPotentialTerm'_W2_finset` `ofPotentialTerm'_W3_finset` `ofPotentialTerm'_W4_finset` `ofPotentialTerm'_K2_finset` `ofPotentialTerm'_topYukawa_finset` `ofPotentialTerm'_bottomYukawa_finset`
`ofPotentialTerm'_topYukawa_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.topYukawa` `qHu` `Q10`	—	—
`ofPotentialTerm'_β_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.β` `qHu` `Q5`	—	—
`ofPotentialTerm'_μ_finset` 📖	mathematical	—	`ofPotentialTerm'` `SuperSymmetry.SU5.PotentialTerm.μ` `qHd` `qHu`	—	—
`ofPotentialTerm_empty` 📖	mathematical	—	`ofPotentialTerm` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	—
`ofPotentialTerm_mono` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`ofPotentialTerm`	—	`ofFieldLabel_mono` `subset_def`
`ofPotentialTerm_subset_ofPotentialTerm'` 📖	mathematical	—	`ofPotentialTerm` `ofPotentialTerm'`	—	`ofPotentialTerm'_μ_finset` `ofPotentialTerm'_β_finset` `ofPotentialTerm'_W2_finset` `ofPotentialTerm'_W3_finset` `ofPotentialTerm'_W4_finset` `ofPotentialTerm'_K2_finset` `ofPotentialTerm'_topYukawa_finset` `ofPotentialTerm'_bottomYukawa_finset`

---

← Back to Index