OAI/Analysis/PathSelection/ScalarRoots.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Scalar roots, reflection and real algebraic roots.

  1. lemma OAI.DegeneratingTrees.ScalarEvaluation.monic_irreducible_has_root line 18
  2. theorem OAI.DegeneratingTrees.ScalarEvaluation.isAlgClosed line 95
  3. def OAI.DegeneratingTrees.ScalarEvaluation.Reflected line 113
  4. lemma OAI.DegeneratingTrees.ScalarEvaluation.eq_of_eventuallyEq line 116
  5. def OAI.DegeneratingTrees.ScalarEvaluation.reflectedValue line 119
  6. lemma OAI.DegeneratingTrees.ScalarEvaluation.reflectedValue_spec line 120
  7. lemma OAI.DegeneratingTrees.ScalarEvaluation.reflectedValue_involutive line 124
  8. def OAI.DegeneratingTrees.ScalarEvaluation.conjugation line 131
  9. lemma OAI.DegeneratingTrees.ScalarEvaluation.conjugation_spec line 149
  10. lemma OAI.DegeneratingTrees.ScalarEvaluation.conjugation_const line 153
  11. lemma OAI.DegeneratingTrees.ScalarEvaluation.conjugation_involutive line 159
  12. def OAI.DegeneratingTrees.ScalarEvaluation.realPart line 162
  13. lemma OAI.DegeneratingTrees.ScalarEvaluation.mem_realPart line 165
  14. lemma OAI.DegeneratingTrees.ScalarEvaluation.sumSq_eval_nonneg line 178
  15. lemma OAI.DegeneratingTrees.ScalarEvaluation.realPart_semireal line 191
  16. lemma OAI.DegeneratingTrees.odd_multiset_involution_fixed line 210
  17. lemma OAI.DegeneratingTrees.fixed_subfield_odd_root line 239
  18. lemma OAI.DegeneratingTrees.ScalarEvaluation.realPart_square_or_neg line 281
  19. theorem OAI.DegeneratingTrees.ScalarEvaluation.realPart_isRealClosed line 305