instance
instModuleSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRing
{K : Type u_1}
[Field K]
:
Module { x // x ∈ NumberField.ringOfIntegers K } { x // x ∈ NumberField.ringOfIntegers K }
Equations
- One or more equations did not get rendered due to their size.
theorem
exists_int_sModEq
{K : Type u_1}
[Field K]
(pb : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K })
(x : { x // x ∈ NumberField.ringOfIntegers K })
:
∃ n, x ≡ ↑n [SMOD Ideal.span {pb.gen}]
theorem
gen_ne_zero
{K : Type u_1}
[Field K]
{pb : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }}
[NumberField K]
(hpr : Prime (↑(RingOfIntegers.norm ℚ) pb.gen))
:
pb.gen ≠ 0
theorem
quotient_not_trivial
{K : Type u_1}
[Field K]
{pb : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }}
[NumberField K]
(hpr : Prime (↑(RingOfIntegers.norm ℚ) pb.gen))
:
Nontrivial ({ x // x ∈ NumberField.ringOfIntegers K } ⧸ Ideal.span {pb.gen})
theorem
SModEq.Ideal_def
{R : Type u_1}
[CommRing R]
(I : Ideal R)
(x : R)
(y : R)
:
x ≡ y [SMOD I] ↔ ↑(Ideal.Quotient.mk I) x = ↑(Ideal.Quotient.mk I) y
instance
instModuleSubtypeRatMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommRingToEuclideanDomainFieldAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersSubtypeMemSubalgebraToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRing
{K : Type u_1}
[Field K]
[NumberField K]
:
Module { x // x ∈ NumberField.ringOfIntegers ℚ } { x // x ∈ NumberField.ringOfIntegers K }
Equations
- One or more equations did not get rendered due to their size.
instance
instSMulSubtypeRatMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommRingToEuclideanDomainFieldAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersSubtypeMemSubalgebraToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegers
{K : Type u_1}
[Field K]
[NumberField K]
:
SMul { x // x ∈ NumberField.ringOfIntegers ℚ } { x // x ∈ NumberField.ringOfIntegers K }
Equations
- One or more equations did not get rendered due to their size.
theorem
norm_intCast
{K : Type u_1}
[Field K]
[NumberField K]
(n : ℤ)
:
↑(RingOfIntegers.norm ℚ) ↑n = ↑(n ^ FiniteDimensional.finrank ℚ K)
theorem
prime_of_norm_prime
{K : Type u_1}
[Field K]
{pb : PowerBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }}
[NumberField K]
(hpr : Prime (↑(RingOfIntegers.norm ℚ) pb.gen))
[IsGalois ℚ K]
:
Prime pb.gen