Documentation Verification Report

IsField

📁 Source: Mathlib/Algebra/Field/IsField.lean

Statistics

Metric	Count
Definitions `IsField`, `toField`, `toSemifield`	3
Theorems `toIsField`, `exists_pair_ne`, `isDomain`, `mul_comm`, `mul_inv_cancel`, `nontrivial`, `toIsField`, `instIsDomain`, `not_isField_of_subsingleton`, `uniq_inv_of_isField`	10
Total	13

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsField` 📖	mathematical	—	`IsField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield`	—	`Semifield.toIsField`

IsField

Definitions

Name	Category	Theorems
`toField` 📖	CompOp	—
`toSemifield` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pair_ne` 📖	—	`IsField`	—	—	—
`isDomain` 📖	mathematical	`IsField`	`IsDomain`	—	`mul_inv_cancel` `mul_comm` `mul_one` `mul_assoc` `exists_pair_ne`
`mul_comm` 📖	mathematical	`IsField`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`mul_inv_cancel` 📖	mathematical	`IsField`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`nontrivial` 📖	mathematical	`IsField`	`Nontrivial`	—	`exists_pair_ne`

Semifield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsField` 📖	mathematical	—	`IsField` `DivisionSemiring.toSemiring` `toDivisionSemiring`	—	`Nontrivial.exists_pair_ne` `toNontrivial` `CommSemiring.mul_comm` `mul_inv_cancel₀`

(root)

Definitions

Name	Category	Theorems
`IsField` 📖	CompData	48 math math: `IsArtinianRing.isField_of_isDomain`, `NumberField.RingOfIntegers.not_isField`, `Ring.isField_iff_isSimpleOrder_ideal`, `ringKrullDim_eq_one_iff_of_isLocalRing_isDomain`, `AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponents`, `Finite.isField_of_domain`, `IsFractionRing.surjective_iff_isField`, `Ideal.IsField.of_isPrincipalIdealRing_polynomial`, `PrimeSpectrum.t1Space_iff_isField`, `Ideal.polynomial_not_isField`, `Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal`, `IsLocalRing.subsingleton_cotangentSpace_iff`, `IsLocalRing.finrank_cotangentSpace_eq_zero_iff`, `Int.not_isField`, `Fintype.not_isField_of_card_not_prime_pow`, `Field.toIsField`, `Algebra.TensorProduct.isField_of_isAlgebraic`, `Polynomial.not_isField`, `Finite.isDomain_to_isField`, `IsDiscreteValuationRing.not_isField`, `Subalgebra.isField_of_algebraic`, `IsLocalRing.isField_iff_maximalIdeal_eq`, `Semifield.toIsField`, `Algebra.TensorProduct.not_isField_of_transcendental`, `PowerSeries.not_isField`, `IsSimpleRing.isField_center`, `IsArtinianRing.isField_of_isReduced_of_isLocalRing`, `Ring.not_isField_iff_exists_prime`, `Ring.KrullDimLE.isField_of_isDomain`, `Valuation.valuationSubring_not_isField`, `isSimpleRing_iff_isField`, `IsLocalization.AtPrime.not_isField`, `Ring.KrullDimLE.isField_of_isReduced`, `IntermediateField.LinearDisjoint.isField_of_isAlgebraic'`, `AlgebraicGeometry.isField_of_universallyClosed`, `not_isField_of_subsingleton`, `PrimeSpectrum.subsingleton_iff_isField_of_isReduced`, `Ring.isField_iff_maximal_bot`, `IntermediateField.LinearDisjoint.isField_of_forall`, `Ring.not_isField_of_ne_of_ne`, `AlgebraicGeometry.isField_of_isIntegral_of_subsingleton`, `Algebra.IsIntegral.isField_iff_isField`, `Submodule.traceDual_top`, `Ideal.Quotient.maximal_ideal_iff_isField_quotient`, `IntermediateField.LinearDisjoint.isField_of_isAlgebraic`, `Algebra.FormallyUnramified.isField_of_isAlgClosed_of_isLocalRing`, `Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top`, `FunctionField.ringOfIntegers.not_isField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDomain` 📖	mathematical	—	`IsDomain` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IsField.isDomain` `Semifield.toIsField`
`not_isField_of_subsingleton` 📖	mathematical	—	`IsField`	—	`IsField.exists_pair_ne`
`uniq_inv_of_isField` 📖	mathematical	`IsField` `Ring.toSemiring`	`ExistsUnique` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`existsUnique_of_exists_of_unique` `IsField.mul_inv_cancel` `mul_one` `mul_assoc` `IsField.mul_comm` `one_mul`

---

← Back to Index