NumberField.RingOfIntegers.not_isField
theorem NumberField.RingOfIntegers.not_isField :
∀ (K : Type u_1) [inst : Field K] [nf : NumberField K], ¬IsField ↥(NumberField.ringOfIntegers K)
The theorem states that the ring of integers of a given number field is not a field itself. In more detail, for any number field 'K', the ring of integers of 'K', which is the integral closure of the integers in the number field, cannot have the structure of a field.
More concisely: The ring of integers of a number field is not a field.
|
Int.not_isField
theorem Int.not_isField : ¬IsField ℤ
This theorem asserts that the set of integers `ℤ`, under its usual ring structure, does not form a field. In mathematical terms, it means that while integers can be added, subtracted, and multiplied to get another integer (the properties of a ring), they cannot always be divided by each other to get another integer (a necessary property for fields). Therefore, the integers do not satisfy all the properties required for a field.
More concisely: The integers `ℤ` do not form a field under their ring structure.
|