Theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso

Modification history

2026-09-16 13:44

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

fix(Algebra/MonoidWithZeroHom): normalize to `.toMonoidWithZeroHom` (#43728) …

Modified IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso View on Github →

2026-07-09 14:13

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

refactor(NumberTheory): make `adicCompletion` a one-field structure (#41526) …

Added IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso View on Github →