IntegerCountObject.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DerivedBar.ParityBridge.countObject line 36
Source documentation
The original r-count object, with exactly the original scalar and inflated actions.
```
abbrev countObject (r : ℕ) :=
…
```
def OAI.DerivedBar.ParityBridge.countObjectComparison line 43
Source documentation
The proved genuine shift comparison, with its target named for downstream use.
```
def countObjectComparison (r : ℕ) :
    ((chainToIntegerDerived D).obj
      ((derivedTensorIterate k D X r).obj ((chainQ D).obj Z)))⟦(r:ℤ)⟧ ≅ countObject k D X N r :=
…
```
Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.chainQ, OAI.DerivedBar.ParityBridge.countObject