BoundPlaneDim

📁 Source: PhysLean/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/BoundPlaneDim.lean

Statistics

Metric	Count
Definitions ExistsPlane	1
Theorems exists_plane_exists_basis, plane_exists_dim_le_7	2
Total	3

SMRHN.PlusU1

Definitions

Name	Category	Theorems
ExistsPlane 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_plane_exists_basis 📖	mathematical	ExistsPlane	ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SMRHN.PlusU1 ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule	—	eleven_dim_plane_of_no_sols_exists
plane_exists_dim_le_7 📖	—	ExistsPlane	—	—	exists_plane_exists_basis ACCSystemCharges.instFiniteRatCharges

---

← Back to Index