Commit 2024-07-09 14:08 e90957ea

View on Github →

style(DedekindDomain/AdicValuation): fix some snake_case to lowerCamelCase (#14533) In some theorem names, int_valuation was still used instead of intValuation, and this PR fixes this.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.le_max_iff_min_le

deleted theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_add_le_max'

deleted theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_mul'

deleted theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_one'

deleted theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_zero'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le

deleted theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer

deleted theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd

deleted theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd

deleted theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero'

deleted theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero

deleted theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_zero_le

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean