Theorem IsDedekindDomain.HeightOneSpectrum.asIdeal_injective

Modification history

2026-05-23 07:31
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat(NumberTheory/NumberField/Completion/FinitePlace): add multiplicity lemmas (#39008) …
Added IsDedekindDomain.HeightOneSpectrum.asIdeal_injectiveView on Github →