OAI/RingTheory/Kurosh/LimitEvaluation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of free polynomials in the ultraproduct.

  1. instance OAI.KuroshConstruction.ultraLimitAlgebraInst line 21
  2. def OAI.KuroshConstruction.tailFreeValue line 27
  3. def OAI.KuroshConstruction.ultraTailFreeEval line 34
  4. lemma OAI.KuroshConstruction.ultraFree_evaluate line 57
  5. def OAI.KuroshConstruction.tailPolynomialValue line 77
  6. lemma OAI.KuroshConstruction.ultraPolynomial_evaluate line 81