Permutations

📁 Source: PhysLean/QFT/QED/AnomalyCancellation/Permutations.lean

Statistics

Metric	Count
Definitions `FamilyPermutations`, `PermGroup`, `chargeMap`, `instGroupPermGroup`, `permCharges`, `permOfInjection`, `permThree`, `permThreeInj`, `permTwo`, `permTwoInj`	10
Theorems `FamilyPermutations_anomalyFreeLinear_apply`, `FamilyPermutations_charges_apply`, `Prop_three`, `Prop_two`, `accCube_invariant`, `accGrav_invariant`, `chargeMap_apply`, `permThreeInj_fst`, `permThreeInj_fst_apply`, `permThreeInj_snd`, `permThreeInj_snd_apply`, `permThreeInj_thd`, `permThreeInj_thd_apply`, `permThree_fst`, `permThree_snd`, `permThree_thd`, `permTwoInj_fst`, `permTwoInj_fst_apply`, `permTwoInj_snd`, `permTwoInj_snd_apply`, `permTwo_fst`, `permTwo_snd`	22
Total	32

PureU1

Definitions

Name	Category	Theorems
`FamilyPermutations` 📖	CompOp	9 math math: `sort_perm`, `lineInPlaneCond_perm`, `FamilyPermutations_anomalyFreeLinear_apply`, `FamilyPermutations_charges_apply`, `Odd.lineInCubicPerm_permute`, `VectorLikeEvenPlane.vectorLikeEven_in_span`, `Even.lineInCubicPerm_permute`, `Even.lineInCubicPerm_in_plane`, `constAbs_perm`
`PermGroup` 📖	CompOp	2 math math: `accCube_invariant`, `accGrav_invariant`
`chargeMap` 📖	CompOp	1 math math: `chargeMap_apply`
`instGroupPermGroup` 📖	CompOp	2 math math: `accCube_invariant`, `accGrav_invariant`
`permCharges` 📖	CompOp	2 math math: `accCube_invariant`, `accGrav_invariant`
`permOfInjection` 📖	CompOp	—
`permThree` 📖	CompOp	3 math math: `permThree_snd`, `permThree_fst`, `permThree_thd`
`permThreeInj` 📖	CompOp	6 math math: `permThreeInj_fst`, `permThreeInj_snd_apply`, `permThreeInj_thd_apply`, `permThreeInj_thd`, `permThreeInj_fst_apply`, `permThreeInj_snd`
`permTwo` 📖	CompOp	2 math math: `permTwo_fst`, `permTwo_snd`
`permTwoInj` 📖	CompOp	4 math math: `permTwoInj_fst_apply`, `permTwoInj_snd_apply`, `permTwoInj_fst`, `permTwoInj_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FamilyPermutations_anomalyFreeLinear_apply` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystemGroupAction.group` `FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.linSolRep`	—	—
`FamilyPermutations_charges_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystemGroupAction.group` `FamilyPermutations` `ACCSystemGroupAction.groupInst` `ACCSystemGroupAction.rep`	—	—
`Prop_three` 📖	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystemGroupAction.group` `FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.linSolRep`	—	—	`permThree_thd` `permThree_snd` `permThree_fst` `FamilyPermutations_anomalyFreeLinear_apply`
`Prop_two` 📖	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule` `ACCSystemGroupAction.group` `FamilyPermutations` `ACCSystemGroupAction.instGroupGroup` `ACCSystemGroupAction.linSolRep`	—	—	`permTwo_snd` `permTwo_fst` `FamilyPermutations_anomalyFreeLinear_apply`
`accCube_invariant` 📖	mathematical	—	`HomogeneousCubic` `ACCSystemCharges.Charges` `PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `accCube` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PermGroup` `instGroupPermGroup` `permCharges`	—	`accCube_explicit`
`accGrav_invariant` 📖	mathematical	—	`ACCSystemCharges.Charges` `PureU1Charges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `accGrav` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `PermGroup` `instGroupPermGroup` `permCharges`	—	—
`chargeMap_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `chargeMap`	—	—
`permThreeInj_fst` 📖	mathematical	—	`permThreeInj`	—	—
`permThreeInj_fst_apply` 📖	mathematical	—	`permThreeInj` `permThreeInj_fst`	—	`permThreeInj_fst`
`permThreeInj_snd` 📖	mathematical	—	`permThreeInj`	—	—
`permThreeInj_snd_apply` 📖	mathematical	—	`permThreeInj` `permThreeInj_snd`	—	`permThreeInj_snd`
`permThreeInj_thd` 📖	mathematical	—	`permThreeInj`	—	—
`permThreeInj_thd_apply` 📖	mathematical	—	`permThreeInj` `permThreeInj_thd`	—	`permThreeInj_thd`
`permThree_fst` 📖	mathematical	—	`permThree`	—	`permThree.eq_1` `permOfInjection.eq_1` `permThreeInj_fst` `permThreeInj_fst_apply`
`permThree_snd` 📖	mathematical	—	`permThree`	—	`permThree.eq_1` `permOfInjection.eq_1` `permThreeInj_snd` `permThreeInj_snd_apply`
`permThree_thd` 📖	mathematical	—	`permThree`	—	`permThree.eq_1` `permOfInjection.eq_1` `permThreeInj_thd` `permThreeInj_thd_apply`
`permTwoInj_fst` 📖	mathematical	—	`permTwoInj`	—	—
`permTwoInj_fst_apply` 📖	mathematical	—	`permTwoInj` `permTwoInj_fst`	—	`permTwoInj_fst`
`permTwoInj_snd` 📖	mathematical	—	`permTwoInj`	—	—
`permTwoInj_snd_apply` 📖	mathematical	—	`permTwoInj` `permTwoInj_snd`	—	`permTwoInj_snd`
`permTwo_fst` 📖	mathematical	—	`permTwo`	—	`permTwo.eq_1` `permOfInjection.eq_1` `permTwoInj_fst` `permTwoInj_fst_apply`
`permTwo_snd` 📖	mathematical	—	`permTwo`	—	`permTwo.eq_1` `permOfInjection.eq_1` `permTwoInj_snd` `permTwoInj_snd_apply`

---

← Back to Index