Rat.numberField_discr
theorem Rat.numberField_discr : NumberField.discr ℚ = 1
This theorem states that the absolute discriminant of the number field of rational numbers, denoted as `ℚ`, is 1. In the context of number fields, the absolute discriminant can be thought of as a measure of the complexity of the number field. It's computed using a specific basis of the ring of integers of the number field. Here, it's stating that for the field of rational numbers, this measure is 1, indicating its simplicity.
More concisely: The absolute discriminant of the ring of integers in the number field of rational numbers is equal to 1.
|
NumberField.discr_rat
theorem NumberField.discr_rat : NumberField.discr ℚ = 1
This theorem, referred to as an **Alias** of `Rat.numberField_discr`, states that the absolute discriminant of the number field `ℚ` (the set of rational numbers) is 1. In more mathematical terms, it asserts that the discriminant of the algebraic number field formed by the rational numbers, computed with respect to the integer basis of the field, is equal to 1.
More concisely: The discriminant of the algebraic number field formed by the rational numbers, with respect to the integer basis, equals 1.
|
Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral
theorem Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral :
∀ {ι : Type u_2} {ι' : Type u_3} (K : Type u_1) [inst : Field K] [inst_1 : DecidableEq ι] [inst_2 : DecidableEq ι']
[inst_3 : Fintype ι] [inst_4 : Fintype ι'] [inst_5 : NumberField K] {b : Basis ι ℚ K} {b' : Basis ι' ℚ K},
(∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)) →
(∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑b) i j)) → Algebra.discr ℚ ⇑b = Algebra.discr ℚ ⇑b'
The theorem `Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral` states that for any number field `K` with two distinct bases `b` and `b'` over the rational numbers `ℚ`, indexed by types `ι` and `ι'` respectively, if every matrix element of the transformation from `b` to `b'` is an integral element over the integers `ℤ`, and similarly every matrix element of the transformation from `b'` to `b` is also an integral element over `ℤ`, then the discriminants of these two bases are equal. Here, the discriminant of a basis is defined as the determinant of the trace matrix of this basis.
More concisely: If two number field bases over the rational numbers have transformations between them whose matrix elements are integral elements over the integers, then their discriminants are equal.
|