PR summary ae61e80b6c

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

In #14752 we're updating the definition of Valued defining a SubgroupWithZero and the like. Do you mind putting this PR on hold (as WIP) perhaps marking that it "depends" on #14752? This won't probably be true, but at least you'll get a message from GitHub as soon as that one is merged.

Thanks for pointing out the interaction with the other PR, @faenuccio. How would the underlying definition of Valued affect these constructions? They're really valid over any Valuation. I can move the ideal and submodule constructions to be directly on Valuation.integer, which would decouple them even further from the Valued typeclass. Then the only things that would rely on Valued would be the clopen statements, which would remain true regardless, since you're not changing the underlying topology.

These constructions are factored out from the IsLinearTopology PR which allows for evaluation of power series over Z_p or Q_p. I'm hoping to define that to be able to state Strassman's theorem.

Thanks for pointing out the interaction with the other PR, @faenuccio. How would the underlying definition of Valued affect these constructions? They're really valid over any Valuation. I can move the ideal and submodule constructions to be directly on Valuation.integer, which would decouple them even further from the Valued typeclass. Then the only things that would rely on Valued would be the clopen statements, which would remain true regardless, since you're not changing the underlying topology.

These constructions are factored out from the IsLinearTopology PR which allows for evaluation of power series over Z_p or Q_p. I'm hoping to define that to be able to state Strassman's theorem.

I need to split the other PR in two following a reviewer's request. As soon as I do, I'll have a clearer vision and will (hopefully be able to) answer your questions... 😅

This pull request has conflicts, please merge master and resolve them.

Superseded by #26829.