Theorems · Definition · field theory
IsField.toField
{R : Type u} → [inst : Ring R] → IsField R → Field RTransferring from IsField to Field.
- Defined in
- Mathlib.Algebra.Field.IsField
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Fieldstatement · cited by 7,404
- Semifieldproof · cited by 439
- IsFieldstatement and proof · cited by 103
- IsField.toSemifieldproof · cited by 3
- Semifield.nnqsmulproof · cited by 1
- Semifield.div_eq_mul_invproof · cited by 0
- Semifield.inv_zeroproof · cited by 0
- Semifield.mul_inv_cancelproof · cited by 0
- Semifield.nnqsmul_defproof · cited by 0
- Semifield.nnratCast_defproof · cited by 0
- Semifield.zpow_neg'proof · cited by 0
Cited by22
Results whose statement or proof uses this declaration.
- Algebra.FormallyUnramified.isReduced_of_fieldproof · cited by 6
- Polynomial.induction_of_Splits_of_injective_of_surjectiveproof · cited by 4
- IsField.localization_map_bijectiveproof · cited by 3
- Polynomial.resultant_eq_prod_evalproof · cited by 3
- IsBaseChange.lift_rank_eqproof · cited by 3
- isField_of_isIntegral_of_isField'proof · cited by 3
- Subalgebra.LinearDisjoint.of_isFieldproof · cited by 3
- Polynomial.not_weaklyQuasiFiniteAtproof · cited by 2
- IsLocalization.AtPrime.not_isFieldproof · cited by 2
- AlgebraicGeometry.geometrically_eq_universallyproof · cited by 2
- Algebra.TensorProduct.not_isField_of_transcendentalproof · cited by 1
- IsLocalRing.finrank_CotangentSpace_eq_one_iffproof · cited by 1