Commit 2023-06-26 15:15 186ec0c6

View on Github →

feat: port RingTheory.DedekindDomain.SelmerGroup (#5478)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

added def IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero

added def IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod

added def IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun

added theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq

added theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq

added def IsDedekindDomain.selmerGroup.fromUnit

added def IsDedekindDomain.selmerGroup.fromUnitLift

added theorem IsDedekindDomain.selmerGroup.fromUnitLift_injective

added theorem IsDedekindDomain.selmerGroup.fromUnit_ker

added theorem IsDedekindDomain.selmerGroup.monotone

added def IsDedekindDomain.selmerGroup.valuation

added theorem IsDedekindDomain.selmerGroup.valuation_ker_eq

added def IsDedekindDomain.selmerGroup