[Merged by Bors] - feat(Algebra/Module/Submodule/Ker): restricting a linear map to its kernel

[faenuccio]

We add the lemma saying that restricting a linear map to its kernel yields the zero map. In passing, we generalise a couple of results from linear to semilinear maps.

---

[github-actions]

PR summary ff0d132afd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ domRestrict_ker_self

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.

[wwylele]

Suggested change

	lemma domRestrict_ker_zero (f : M →ₛₗ[τ₁₂] M₂) : f.domRestrict f.ker = 0 := by
	lemma domRestrict_ker_eq_zero (f : M →ₛₗ[τ₁₂] M₂) : f.domRestrict f.ker = 0 := by

[faenuccio]

I thought about this, but I don't like this name: it seems to say that "the kernel is equal to zero" whereas it is the map.

[wwylele]

I don't think it is ambiguous? If I want to say "kernel is equal to zero", I would name it like "domRestrict{_eq_something}_of_ker_eq_zero"

[faenuccio]

But how would you call the (false) lemma saying "the kernel of domRestrict is zero"?

[themathqueen]

How about just domRestrict_ker? It's a simp lemma anyway.

[faenuccio]

And what about domRestrict_of_ker? What I´d like to stress is that the lemma is not about a kernel but about a domRestrict.

[YaelDillies]

If it were about the kernel, it would be ker_.... domRestrict_ker_self is the name suggested by the naming convention.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[ADedecker]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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