OAI/Algebra/Finitistic/Dimension/PDResidueScalar.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PDResidueScalar.moduleK line 11

   Source documentation

   Name the generic residue scalar structure so concrete square-zero algebras need not unfold their entire construction during typeclass search.

   @[instance_reducible] def moduleK : Module k (PDTensor.Residue (A := A)) := inferInstance
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Residue

2. theorem OAI.LittleFinitistic.PDResidueScalar.towerK line 15