CanonicalBarTermValues.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ArExplicit.BarBalanced.canonicalTermIso_hom_eq line 14
abbrev OAI.ArExplicit.BarBalanced.canonicalTermTmulProof line 18
theorem OAI.ArExplicit.BarBalanced.canonicalTermIso_tmul line 25
Source comment
The characteristic assumption is retained explicitly in the complex-isomorphism interface. Using its defining linear equivalence avoids expanding the complex module structures.
```
theorem canonicalTermIso_tmul [CharP k 2] (n : ℕ)
    (z : EnvelopingBimodule k R (AbsoluteBar.moduleObject k R (n+1))) (x : X) :
    type_of% (canonicalTermTmulProof k R X n z x) :=
…
```
Mentions: OAI.ArExplicit.EnvelopingBimodule, OAI.ArExplicit.AbsoluteBar.moduleObject, OAI.ArExplicit.BarBalanced.canonicalTermTmulProof
theorem OAI.ArExplicit.BarBalanced.canonicalComplexIso_tmul line 31