OAI/Algebra/Finitistic/Dimension/PDResidueRing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PDTensor.residueRingEquiv line 13

   Source documentation

   The right-module quotient used by tensor detection is the underlying vector space of the usual quotient ring A/rad A.

   def residueRingEquiv : Residue (A := A) ≃ₗ[k] A ⧸ Ring.jacobson A :=
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Residue