Three

📁 Source: PhysLean/QFT/QED/AnomalyCancellation/LowDim/Three.lean

Statistics

Metric	Count
Definitions solOfLinear	1
Theorems cube_for_linSol, cube_for_linSol', solOfLinear_surjects, three_sol_zero	4
Total	5

PureU1.Three

Definitions

Name	Category	Theorems
solOfLinear 📖	CompOp	1 math math: solOfLinear_surjects

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cube_for_linSol 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 HomogeneousCubic ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun ACCSystem.cubicACC	—	cube_for_linSol'
cube_for_linSol' 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 HomogeneousCubic ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun ACCSystem.cubicACC	—	pureU1_linear PureU1.accCube_explicit
solOfLinear_surjects 📖	mathematical	—	solOfLinear	—	three_sol_zero
three_sol_zero 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemQuad.QuadSols.toLinSols ACCSystem.Sols.toQuadSols	—	cube_for_linSol ACCSystem.Sols.cubicSol

---

← Back to Index