mem_eqLocus — Mathlib

English

The equalizer submodule of f and g corresponds to the equalizer submonoid of their additive homomorphisms.

Русский

Равноправный элемент подмодуля (равносильный) f и g соответствует равноправному элементу их аддитивных гомоморфизмов.

LaTeX

$$$(eqLocus\ f\ g).toAddSubmonoid = (f : M \to+ M_2).eqLocusM g$$$

Lean4

@[simp]
theorem mem_eqLocus {x : M} {f g : F} : x ∈ eqLocus f g ↔ f x = g x :=
  Iff.rfl

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