Theorem NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm

Modification history

2026-03-07 22:10
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat(NumberTheory/NumberField/FinitePlaces): `Module.Finite (v.adicCompletion K) (w.adicCompletion L)` (#36067) …
Deleted NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNormView on Github →
2026-03-02 10:51
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
refactor: use 1-field structure to define the `WithVal` type synonym (#34049) …
Modified NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNormView on Github →
2025-03-01 13:14
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat: `WithVal` type synonym and refactor of `HeightOneSpectrum.adicCompletion` (#22055) …
Modified NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNormView on Github →
2025-02-28 20:55
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: renaming and documentation for `NumberField.FinitePlace` (#22407)
Added NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNormView on Github →