Commit 2025-02-14 14:49 a4c33305

View on Github →

chore(DedekindDomain/AdicCompletion): generalise algebra instance to separate rings (#21301) This is analogous to #19466. From FLT

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion'

modified theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion

modified theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion