PadicInt.smul_submodule_relindex usage in broader proof

Stream: FLT

[Aaron Hill]

I have a sorry-free (but still messy) proof of PadicInt.smul_submodule_relindex for the special case of s = (1 : Submodule ℤ_[p] ℚ_[p]). Currently, smul_submodule_relindex is only ever used with that special case (in distribHaarChar_padic_padicInt). Is this lemma going to eventually be needed in the full generality, or would it be okay to replace it with the Submodule.one special case?

[Kevin Buzzard]

@Yaël Dillies I think all this was your doing?

[Yaël Dillies]

Sure yeah it's fine to restrict to the special case!

[Aaron Hill]

Sounds good - I'll clean up the proof and open a pr

[Yaël Dillies]

For future reference, the special case of PadicInt.smul_submodule_relindex is used to prove properties of the Haar measure on the p-adics, and those properties can in turn be used to prove the general case of PadicInt.smul_submodule_relindex