Theorem IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem

Modification history

2025-01-17 05:44
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
chore: restore `def` to `adicCompletion` (#20796) …
Added IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_memView on Github →