Commit 2026-03-07 22:10 447d413d
View on Github →feat(NumberTheory/NumberField/FinitePlaces): Module.Finite (v.adicCompletion K) (w.adicCompletion L) (#36067)
Let v : HeightOneSpectrum (𝓞 K) and w : HeightOneSpectrum (𝓞 L) be such that we have Algebra (v.adicCompletion K) (w.adicCompletion L). If this algebra gives continuous scalar multiplication and we have IsScalarTower K (v.adicCompletion K) (w.adicCompletion L), then w.adicCompletion L is finite-dimensional over v.adicCompletion K.
Estimated changes
deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm
deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply
deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max
deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one