Documentation Verification Report

Inertia

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

Statistics

Metric	Count
Definitions `inertiaDeg`	1
Theorems `absNorm_eq_pow_inertiaDeg`, `absNorm_eq_pow_inertiaDeg'`, `absNorm_eq_pow_inertiaDeg_of_liesOver`, `inertiaDeg_algebraMap`, `inertiaDeg_algebra_tower`, `inertiaDeg_bot`, `inertiaDeg_comap_eq`, `inertiaDeg_map_eq`, `inertiaDeg_ne_zero`, `inertiaDeg_of_subsingleton`, `inertiaDeg_pos`	11
Total	12

Ideal

Definitions

Name	Category	Theorems
`inertiaDeg` 📖	CompOp	30 math math: `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `inertiaDeg_comap_eq`, `inertiaDeg_algebraMap`, `absNorm_eq_pow_inertiaDeg'`, `relNorm_eq_pow_of_isPrime_isGalois`, `absNorm_eq_pow_inertiaDeg_of_liesOver`, `IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg`, `sum_ramification_inertia`, `IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq`, `inertiaDeg_eq_of_isGalois`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one`, `IsCyclotomicExtension.Rat.inertiaDeg_eq`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'`, `inertiaDeg_eq_of_isGaloisGroup`, `inertiaDeg_pos`, `inertiaDeg_of_subsingleton`, `ramificationIdx_mul_inertiaDeg_of_isLocalRing`, `Factors.finrank_pow_ramificationIdx`, `inertiaDeg_bot`, `inertiaDeg_algebra_tower`, `inertiaDegIn_eq_inertiaDeg`, `absNorm_eq_pow_inertiaDeg`, `inertiaDeg_le_finrank`, `IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd`, `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd`, `inertiaDeg_map_eq`, `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime`, `relNorm_eq_pow_of_isMaximal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absNorm_eq_pow_inertiaDeg` 📖	mathematical	`Prime` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring`	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Monoid.toPow` `Nat.instMonoid` `inertiaDeg` `Int.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing` `span` `Int.instSemiring` `Set` `Set.instSingletonSet`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `inertiaDeg_algebraMap` `IsPrincipalIdealRing.isDedekindDomain` `Int.instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Module.free_of_finite_type_torsion_free'` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroup.instFGInt` `instIsTorsionFreeIntOfIsAddTorsionFree` `Int.instIsAddTorsionFree` `absNorm_span_singleton` `Algebra.norm_self` `absNorm_eq_pow_inertiaDeg_of_liesOver` `span_singleton_prime` `Prime.ne_zero`
`absNorm_eq_pow_inertiaDeg'` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Monoid.toPow` `Nat.instMonoid` `inertiaDeg` `Int.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing` `span` `Int.instSemiring` `Set` `Set.instSingletonSet`	—	`absNorm_eq_pow_inertiaDeg` `Nat.prime_iff_prime_int`
`absNorm_eq_pow_inertiaDeg_of_liesOver` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Monoid.toPow` `Nat.instMonoid` `inertiaDeg`	—	`IsPrime.isMaximal` `IsDedekindDomainDvr.ring_dimensionLEOne` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.isDedekindDomainDvr` `IsDomain.toNontrivial` `Submodule.cardQuot_apply` `inertiaDeg_algebraMap` `Module.natCard_eq_pow_finrank` `module_finite_of_liesOver`
`inertiaDeg_algebraMap` 📖	mathematical	—	`inertiaDeg` `Module.finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Quotient.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Algebra.toModule` `Quotient.commSemiring` `Quotient.algebraOfLiesOver`	—	`instIsTwoSided_1` `inertiaDeg.eq_1` `over_def`
`inertiaDeg_algebra_tower` 📖	mathematical	—	`inertiaDeg`	—	`over_def` `LiesOver.over` `LiesOver.trans` `instIsTwoSided_1` `Eq.le` `Module.finrank_mul_finrank` `IsScalarTower.of_algebraMap_eq` `IsScalarTower.algebraMap_apply` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`
`inertiaDeg_bot` 📖	mathematical	—	`inertiaDeg` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Module.finrank` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`instIsTwoSided_1` `inertiaDeg.eq_1` `over_def` `eq_bot_of_liesOver_bot` `Algebra.finrank_eq_of_equiv_equiv` `instIsTwoSidedBot`
`inertiaDeg_comap_eq` 📖	mathematical	—	`inertiaDeg` `comap` `AlgEquiv` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgEquiv.instFunLike` `AlgHomClass.toRingHomClass` `EquivLike.toFunLike` `AlgEquiv.instEquivLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`	—	`RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `comap_coe` `comap_comap` `AlgHom.algHomClass` `AlgEquiv.toAlgHom_toRingHom` `AlgHom.comp_algebraMap` `comap_liesOver` `inertiaDeg_algebraMap` `LinearEquiv.finrank_eq` `instIsTwoSided_1` `inertiaDeg.eq_1`
`inertiaDeg_map_eq` 📖	mathematical	—	`inertiaDeg` `map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike`	—	`AlgEquivClass.toRingEquivClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_comap_of_equiv` `inertiaDeg_comap_eq`
`inertiaDeg_ne_zero` 📖	—	—	—	—	`inertiaDeg_pos`
`inertiaDeg_of_subsingleton` 📖	mathematical	—	`inertiaDeg`	—	`Quotient.subsingleton_iff` `IsMaximal.ne_top` `comap_top` `instIsTwoSided_1`
`inertiaDeg_pos` 📖	mathematical	—	`inertiaDeg`	—	`Quotient.nontrivial_of_liesOver_of_isPrime` `IsMaximal.isPrime'` `LT.lt.trans_eq` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `module_finite_of_liesOver` `Quotient.isDomain` `instIsTwoSided_1` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `inertiaDeg_algebraMap`

---

← Back to Index