Theorem NumberField.RingOfIntegers.HeightOneSpectrum.rankOne_hom'_def

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.rankOne_hom'_defView on Github →
2026-03-06 13:45
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872) …
Added NumberField.RingOfIntegers.HeightOneSpectrum.rankOne_hom'_defView on Github →