OAI/Analysis/SeparableQuotients/Positive/ComplexSequences.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.exists_near_unit_annihilating line 24
  2. def OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.chooseNearPair line 71
  3. lemma OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.chooseNearPair_spec line 76
  4. def OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.nearState line 84
  5. def OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.nearPair line 92
  6. def OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.nearNormers line 95
  7. lemma OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.nearState_value line 98
  8. lemma OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.nearState_mono line 109
  9. lemma OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.nearNormers_subset line 114
  10. theorem OAI.SeparableQuotient.Positive.Fields.ComplexTransfer.exists_near_prefix_sequence line 124