eqLocusM_same — Mathlib

English

For any monoid homomorphism f, the equality locus of f with itself is the top submonoid; in other words, f equals itself everywhere.

Русский

Для любого гомоморфизма моноидов f множество точного совпадения f с самим собой равно верхнему подмоноду; то есть f равно самого себя повсюду.

LaTeX

$$$f.\mathrm{eqLocusM} f = \top$$$

Lean4

@[to_additive (attr := simp)]
theorem eqLocusM_same (f : M →* N) : f.eqLocusM f = ⊤ :=
  SetLike.ext fun _ => eq_self_iff_true _

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