[Merged by Bors] - doc: module docstrings for files split off from Topology.Algebra.Module.LinearMap

[ADedecker]

---

[github-actions]

PR summary 8cdcb5f867

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[faenuccio]

Thanks so much! I've left several comments, don't hesitate to ping me again once they're addressed.

[faenuccio]

Suggested change

	* `Submodule.subtypeL S` is the canonical inclusion `S →L[R] M` when `S : Submodule R M`.
	* `Submodule.subtypeL S` is the canonical inclusion `S →L[R] M` when `S : Submodule R M`, seen as a continuous linear map.

Also, beware once more for "canonical"

[ADedecker]

Aren't the mention of the type S →L[R] M and the line below enough?

[faenuccio]

They might be, sure, but I prefer to err by saying more than less. More practically, the sentence seems to say that Submodule.sybtypeL S is the inclusion (which I see as a set-theoretic stuff), while you want to say that it is the inclusion seen as a cont lin map. Not too important, though, so do as you want.

[ADedecker]

Mostly the issue is that I would then have to add it to every single entry in these docstrings, which seems redundant 😅

[ADedecker]

-awaiting-author

[faenuccio]

Thanks again!

bors d+

[mathlib-bors]

✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ADedecker]

Thanks for the quick review!

bors merge

[themathqueen]

I forgot to submit my review last night, aaa, I think I'm too late

[ADedecker]

bors cancel

[mathlib-bors]

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

[ADedecker]

@themathqueen do you have other suggestions to make ? Otherwise I'll re-bors I think.

[themathqueen]

I think it's fine. Thanks! Go ahead and send it to bors! :)

[ADedecker]

Thanks for the extra suggestions!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Post-CI job
• ci (staging) / Build