OAI/RingTheory/Kurosh/RetainedRelations.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Persistence of formal identities and scheduled polynomial relations.

  1. lemma OAI.KuroshConstruction.freeScalarChange_aeval line 10
  2. lemma OAI.KuroshConstruction.constant_free_evaluate line 18
  3. lemma OAI.KuroshConstruction.sequence_formal_retained line 28
  4. lemma OAI.KuroshConstruction.sequence_polynomial_retained line 39
  5. theorem OAI.KuroshConstruction.sequence_scheduled_formal line 55
  6. lemma OAI.KuroshConstruction.sequence_scheduled_constants line 79