OAI/RingTheory/Kurosh/TangentDirections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Independent tangent directions at the universal pair of formal variables.

  1. lemma OAI.KuroshConstruction.letterTuple_liftingInput line 10
  2. def OAI.KuroshConstruction.seedStage line 34