Commit 2023-06-08 06:34 9dff81ad

View on Github →

feat: port NumberTheory.RamificationInertia (#4795)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/RamificationInertia.lean

added theorem Ideal.Factors.finrank_pow_ramificationIdx

added theorem Ideal.Factors.inertiaDeg_ne_zero

added theorem Ideal.Factors.ne_bot

added theorem Ideal.Factors.piQuotientEquiv_map

added theorem Ideal.Factors.piQuotientEquiv_mk

added theorem Ideal.Factors.ramificationIdx_ne_zero

added theorem Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial

added theorem Ideal.FinrankQuotientMap.span_eq_top

added theorem Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count

added theorem Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count

added theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero

added theorem Ideal.Quotient.algebraMap_quotient_of_ramificationIdx_neZero

added theorem Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx

added def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero

added theorem Ideal.finrank_prime_pow_ramificationIdx

added theorem Ideal.finrank_quotient_map

added theorem Ideal.inertiaDeg_algebraMap

added theorem Ideal.inertiaDeg_of_subsingleton

added theorem Ideal.le_comap_of_ramificationIdx_ne_zero

added theorem Ideal.le_comap_pow_ramificationIdx

added theorem Ideal.le_pow_of_le_ramificationIdx

added theorem Ideal.le_pow_ramificationIdx

added def Ideal.powQuotSuccInclusion

added theorem Ideal.powQuotSuccInclusion_injective

added theorem Ideal.quotientToQuotientRangePowQuotSuccAux_mk

added theorem Ideal.quotientToQuotientRangePowQuotSucc_injective

added theorem Ideal.quotientToQuotientRangePowQuotSucc_mk

added theorem Ideal.quotientToQuotientRangePowQuotSucc_surjective

added theorem Ideal.ramificationIdx_bot

added theorem Ideal.ramificationIdx_eq_find

added theorem Ideal.ramificationIdx_eq_zero

added theorem Ideal.ramificationIdx_lt

added theorem Ideal.ramificationIdx_ne_zero

added theorem Ideal.ramificationIdx_of_not_le

added theorem Ideal.ramificationIdx_spec

added theorem Ideal.rank_pow_quot

added theorem Ideal.rank_pow_quot_aux

added theorem Ideal.rank_prime_pow_ramificationIdx

added theorem Ideal.sum_ramification_inertia