Unramified

📁 Source: Mathlib/NumberTheory/RamificationInertia/Unramified.lean

Statistics

Metric	Count
Definitions	0
Theorems of_liesOver, isUnramifiedAt_iff_of_isDedekindDomain, ramificationIdx_eq_one_of_isUnramifiedAt, of_liesOver_of_ne_bot	4
Total	4

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnramifiedAt_iff_of_isDedekindDomain 📖	mathematical	—	IsUnramifiedAt Ideal.ramificationIdx algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Ideal.under	—	Ideal.IsPrime.under Ideal.over_under instIsLocalHomAtPrimeRingHomAlgebraMap Localization.AtPrime.isLocalRing isUnramifiedAt_iff_map_eq Ideal.finiteQuotientOfFreeOfNeBot Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain Int.instIsDomain instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero Ideal.eq_bot_of_comap_eq_bot instNontrivialOfCharZero IsDedekindDomain.toIsDomain IsLocalization.finite instIsFractionRingQuotientIdealResidueField IsAlgebraic.isSeparable_of_perfectField instIsAlgebraicResidueFieldOfIsIntegral PerfectField.ofFinite RingHom.instRingHomClass Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff Ideal.map_comap_le

Algebra.IsUnramifiedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_liesOver 📖	mathematical	—	Algebra.IsUnramifiedAt	—	IsUnramifiedAt.of_liesOver_of_ne_bot Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors Ideal.ne_bot_of_liesOver_of_ne_bot IsDedekindDomain.toIsDomain IsDomain.toNontrivial

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ramificationIdx_eq_one_of_isUnramifiedAt 📖	mathematical	—	ramificationIdx algebraMap CommRing.toCommSemiring CommSemiring.toSemiring under	—	ramificationIdx_eq_one_of_map_localization map_comap_le primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors IsPrime.under over_under instIsLocalHomAtPrimeRingHomAlgebraMap Localization.AtPrime.isLocalRing Algebra.isUnramifiedAt_iff_map_eq

IsUnramifiedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_liesOver_of_ne_bot 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Ideal.primeCompl nonZeroDivisors Semiring.toMonoidWithZero	Algebra.IsUnramifiedAt	—	Ideal.LiesOver.trans Ideal.over_under Ideal.LiesOver.over Algebra.EssFiniteType.of_comp Algebra.EssFiniteType.isNoetherianRing IsDedekindDomainDvr.toIsNoetherian IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr Ideal.IsPrime.under instIsLocalHomAtPrimeRingHomAlgebraMap Localization.AtPrime.isLocalRing Algebra.isUnramifiedAt_iff_map_eq Algebra.isSeparable_tower_bot_of_isSeparable IsLocalRing.toNontrivial Field.instIsLocalRing IsLocalRing.ResidueField.instIsScalarTower_1 Localization.AtPrime.instIsScalarTower_1 le_bot_iff Ideal.map_comap_le IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower IsScalarTower.right Ideal.map_map Localization.AtPrime.map_eq_maximalIdeal RingHom.instRingHomClass Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff not_ne_iff Ideal.ramificationIdx_ne_one_iff Ideal.ramificationIdx_eq_one_of_map_localization Ideal.map_mono LE.le.trans Ideal.map_pow Ideal.pow_right_mono Ideal.map_le_iff_le_comap Eq.le

---

← Back to Index