Commit 2026-11-10 23:17 fef44283

View on Github →

chore(RingTheory): remove unused hypothesis (#45696) Removes unused hypothesis from #45673 in RingTheory.

Estimated changes

Modified Mathlib/NumberTheory/Height/NumberField.lean

Modified Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

modified theorem NumberField.FinitePlace.hasFiniteMulSupport_fun_pow_multiplicity

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

Modified Mathlib/NumberTheory/PrimesCongruentOne.lean

Modified Mathlib/RingTheory/Bialgebra/Hom.lean

modified theorem BialgHom.ext_of_ring

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation/Valuation.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

deleted theorem FractionalIdeal.mul_inv_cancel_of_le_one

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

modified theorem Ideal.irreducible_pow_sup_of_ge

Modified Mathlib/RingTheory/FractionalIdeal/Extended.lean

modified theorem FractionalIdeal.extendedHom_eq_one_iff

modified theorem FractionalIdeal.one_le_extendedHom_iff

Modified Mathlib/RingTheory/FractionalIdeal/Inverse.lean

modified theorem FractionalIdeal.inv_anti_mono

Modified Mathlib/RingTheory/Ideal/Basic.lean

modified theorem Ring.not_isField_of_ne_of_ne

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

modified theorem Ideal.prime_of_irreducible_absNorm_span

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/Multiplicity.lean

modified theorem multiplicity_eq_zero_of_coprime

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

Modified Mathlib/RingTheory/MvPowerSeries/Trunc.lean

modified theorem MvPowerSeries.trunc'_trunc'_pow

modified theorem MvPowerSeries.truncFinset_truncFinset_pow

Modified Mathlib/RingTheory/OrderOfVanishing/Basic.lean

modified theorem Ring.ordFrac_eq_ord

Modified Mathlib/RingTheory/OrderOfVanishing/Noetherian.lean

modified theorem Ring.ordFrac_eq_intValuation

modified theorem Ring.ordMonoidWithZeroHom_eq_intValuation

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

modified theorem Polynomial.coprime_of_root_cyclotomic

modified theorem Polynomial.orderOf_root_cyclotomic_dvd

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

modified theorem PowerSeries.normalized_count_X_eq_of_coe

Modified Mathlib/RingTheory/PowerSeries/Schroder.lean

modified theorem PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq

Modified Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean

modified theorem Associates.count_of_coprime

modified theorem Associates.dvd_of_mem_factors'

modified theorem Associates.le_of_count_ne_zero

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

modified theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors

Modified Mathlib/RingTheory/ZMod/UnitsCyclic.lean

modified theorem ZMod.orderOf_one_add_mul_prime_pow