AnomalyFree

📁 Source: PhysLean/StringTheory/FTheory/SU5/Charges/AnomalyFree.lean

Statistics

Metric	Count
Definitions IsAnomalyFree, instDecidableIsAnomalyFree	2
Theorems isAnomalyFree_map, viable_anomalyFree	2
Total	4

FTheory.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
IsAnomalyFree 📖	MathDef	2 math math: viable_anomalyFree, FTheory.SU5.Quanta.isViable_iff_filter
instDecidableIsAnomalyFree 📖	CompOp	2 math math: viable_anomalyFree, FTheory.SU5.Quanta.isViable_iff_filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAnomalyFree_map 📖	mathematical	IsAnomalyFree	SuperSymmetry.SU5.ChargeSpectrum.map	—	FTheory.SU5.Quanta.mem_liftCharge_iff FTheory.SU5.FiveQuanta.map_liftCharge FTheory.SU5.TenQuanta.map_liftCharge FTheory.SU5.Quanta.HdAnomalyCoefficient_map FTheory.SU5.Quanta.HuAnomalyCoefficient_map FTheory.SU5.FiveQuanta.anomalyCoefficient_of_reduce FTheory.SU5.FiveQuanta.anomalyCoefficient_of_map FTheory.SU5.TenQuanta.anomalyCoefficient_of_reduce FTheory.SU5.TenQuanta.anomalyCoefficient_of_map FTheory.SU5.Quanta.LinearAnomalyCancellation.eq_1
viable_anomalyFree 📖	mathematical	—	SuperSymmetry.SU5.ChargeSpectrum IsAnomalyFree instDecidableIsAnomalyFree viableCharges	—	—

---

← Back to Index