Commit 2026-05-07 17:04 11276bd5

View on Github →

feat(NumberTheory): every number field has a ramified prime (#30666)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Int/Field.lean

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

added theorem Algebra.finrank_eq_one_iff_bijective_algebraMap

Modified Mathlib/NumberTheory/NumberField/Basic.lean

deleted theorem Int.not_isField

Modified Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

added theorem NumberField.not_dvd_discr_iff_forall_liesOver

added theorem NumberField.not_dvd_discr_iff_forall_mem

Created Mathlib/NumberTheory/NumberField/ExistsRamified.lean

added theorem NumberField.exists_not_isUnramifiedAt_int

added theorem NumberField.exists_not_isUnramifiedAt_int_of_isGalois

added theorem NumberField.finrank_eq_one_of_unramified

added theorem bijective_algebraMap_int_of_finite_of_unramified

Modified Mathlib/NumberTheory/RamificationInertia/Inertia.lean

added theorem Ideal.inertiaDeg_pos'

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

Modified Mathlib/RingTheory/Ideal/Maximal.lean

added theorem Ideal.IsMaximal.eq_iff_le

Modified Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

added theorem Ideal.exists_isMaximal_dvd_of_dvd_absNorm'

added theorem Ideal.exists_isMaximal_dvd_of_dvd_absNorm

added theorem Ideal.exists_prime_and_absNorm_eq_pow

added theorem Int.prime_absNorm

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

added theorem Ideal.IsMaximal.ne_bot_of_isIntegral_int

Modified Mathlib/RingTheory/KrullDimension/Basic.lean

added theorem Ideal.IsPrime.isMaximal_of_ne_bot

added theorem Ideal.isMaximal_of_isPrime_of_ne_bot

added theorem Ideal.liesOver_span_iff

added theorem Prime.isMaximal_span_singleton