Theorem IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm

Modification history

2025-02-28 20:55
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: renaming and documentation for `NumberField.FinitePlace` (#22407)
Deleted IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNormView on Github →
2024-12-23 14:21
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat: the product formula for number fields (#20132) …
Added IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNormView on Github →