Theorems · Inductive type · field theory
IsField
(R : Type u) → [Semiring R] → Prop
A predicate to express that a (semi)ring is a (semi)field. This is mainly useful because such a predicate does not contain data, and can therefore be easily transported along ring isomorphisms. Additionally, this is useful when trying to prove that a particular ring structure extends to a (semi)field.
- Defined in
- Mathlib.Algebra.Field.IsField
- Cited by
- 103 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
Cited by109
Results whose statement or proof uses this declaration.
- IsField.toFieldstatement and proof · cited by 22
- Field.toIsFieldstatement · cited by 18
- MulEquiv.isFieldstatement and proof · cited by 14
- Ring.ne_bot_of_isMaximal_of_not_isFieldstatement and proof · cited by 8
- IsLocalRing.isField_iff_maximalIdeal_eqstatement · cited by 8
- IsField.mul_inv_cancelstatement and proof · cited by 7
- Ideal.Quotient.maximal_ideal_iff_isField_quotientstatement · cited by 7
- Polynomial.induction_of_Splits_of_injective_of_surjectiveproof · cited by 4
- Ring.not_isField_iff_exists_primestatement and proof · cited by 4
- IsField.exists_pair_nestatement and proof · cited by 4
- Ideal.Quotient.maximal_of_isFieldstatement and proof · cited by 4
- isField_of_isIntegral_of_isFieldstatement and proof · cited by 4