Documentation Verification Report

BasisLinear

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

Statistics

Metric	Count
Definitions `asBasis`, `asCharges`, `asLinSols`, `coordinateMap`	4
Theorems `asCharges_eq_castSucc`, `asCharges_ne_castSucc`, `asLinSols_val`, `finrank_AnomalyFreeLinear`, `instFiniteRatLinSolsSucc`, `sum_of_vectors`	6
Total	10

PureU1.BasisLinear

Definitions

Name	Category	Theorems
`asBasis` 📖	CompOp	—
`asCharges` 📖	CompOp	3 math math: `asCharges_eq_castSucc`, `asLinSols_val`, `asCharges_ne_castSucc`
`asLinSols` 📖	CompOp	1 math math: `asLinSols_val`
`coordinateMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asCharges_eq_castSucc` 📖	mathematical	—	`asCharges`	—	—
`asCharges_ne_castSucc` 📖	mathematical	—	`asCharges`	—	—
`asLinSols_val` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `asLinSols` `asCharges`	—	—
`finrank_AnomalyFreeLinear` 📖	mathematical	—	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule`	—	`instFiniteRatLinSolsSucc`
`instFiniteRatLinSolsSucc` 📖	mathematical	—	`ACCSystemLinear.LinSols` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.linSolsAddCommMonoid` `ACCSystemLinear.linSolsModule`	—	—
`sum_of_vectors` 📖	mathematical	—	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `PureU1` `ACCSystemLinear.LinSols` `ACCSystemLinear.linSolsAddCommMonoid`	—	`PureU1.sum_of_anomaly_free_linear`

---

← Back to Index