If K,L are number fields, L is a K-algebra, and w is a nonzero prime of the integers of L, then right now mathlib provides a SMul K (adicCompletion L w) instance but not an Algebra K (adicCompletion L w) instance, so one has to tread carefully to avoid diamonds. This is a sorry in DedekindDomain/FiniteAdeleRing/BaseChange.lean but should be fixed in mathlib.
If K,L are number fields, L is a K-algebra, and w is a nonzero prime of the integers of L, then right now mathlib provides a
SMul K (adicCompletion L w)instance but not anAlgebra K (adicCompletion L w)instance, so one has to tread carefully to avoid diamonds. This is asorryinDedekindDomain/FiniteAdeleRing/BaseChange.leanbut should be fixed in mathlib.@YaelDillies is working on this.