OAI/Algebra/DepthFive/ComplexEmbedding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.countable_field_embeds_complex line 13

   Source documentation

   Every countable characteristic-zero field admits an embedding into the complex numbers. This applies to the subfield generated by the finitely many coefficients of a circuit.

   theorem countable_field_embeds_complex (K : Type u) [Field K] [CharZero K] [Countable K] :
       Nonempty (K →+* ℂ) := by
   …