← all areas

Namespace Field 3 theorems

• Countable fields of characteristic zero embed into ℂ Field.nonempty_ringHom_complex_of_countable 0 below · cited by 1 · depth 11
• Kummer descent: p-th roots in a multi-radical extension Field.exists_prod_pow_mul_pow_eq_of_root_mem_adjoin_roots 0 below · cited by 1 · depth 12
• Purely inseparable subextensions when [E:Eᵖ]=p Field.exists_finrank_eq_pow_and_fieldRange_eq_iterateFrobenius_of_isPurelyInseparable 0 below · cited by 1 · depth 20