mem_ker_mkLinearMap_iff — Mathlib

English

For a submonoid S and a linear map g: M → M' with IsLocalizedModule S g, m ∈ ker g holds if and only if there exists r ∈ S with r • m = 0, equivalently described via the equality m ∈ Ker g ⇔ ∃ r ∈ S, r • m = 0.

Русский

Для S и линейного отображения g: M → M' с IsLocalizedModule S g справедливо: m ∈ ker g тогда и только тогда, когда существует r ∈ S такое, что r • m = 0.

LaTeX

$$$m \in \ker g \iff \exists r \in S, r \cdot m = 0$$$

Lean4

theorem mem_ker_mkLinearMap_iff {S : Submonoid R} {m : M} : m ∈ LinearMap.ker (mkLinearMap S M) ↔ ∃ r ∈ S, r • m = 0 :=
  IsLocalizedModule.mem_ker_iff S

Похожие утверждения