equalizer_toSubmodule — Mathlib

English

The underlying submodule of the equalizer of φ and ψ coincides with the locus of equality of φ and ψ.

Русский

Носитель подмодуля равенства φ и ψ совпадает с множеством точек, где φ = ψ.

LaTeX

$$$\operatorname{toSubmodule}(\operatorname{equalizer}(\varphi, \psi)) = \operatorname{eqLocus}(\varphi, \psi)$$$

Lean4

theorem equalizer_toSubmodule {φ ψ : F} : Subalgebra.toSubmodule (equalizer φ ψ) = LinearMap.eqLocus φ ψ :=
  rfl

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