OAI/RingTheory/Kurosh/Lifting.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tangent directions, formal identities, and the algebraic lifting proposition.

  1. def OAI.KuroshConstruction.innerDirection line 14
  2. def OAI.KuroshConstruction.innerTangent line 19
  3. def OAI.KuroshConstruction.constantTuple line 22
  4. def OAI.KuroshConstruction.letterTuple line 25
  5. def OAI.KuroshConstruction.LiftingInput line 28
  6. def OAI.KuroshConstruction.augmentedTuple line 33
  7. def OAI.KuroshConstruction.satisfiesIdentity line 38
  8. def OAI.KuroshConstruction.LiftingStatement line 44