eq_iff — Mathlib

English

For a monoid hom f, f(x) = f(y) if and only if y^{-1} x ∈ ker f.

Русский

Для гомоморфизма f: f(x) = f(y) тогда и только тогда, когда y^{-1} x ∈ ker f.

LaTeX

$$$$ f(x) = f(y) \\iff y^{-1} x \\in \\ker f $$$$

Lean4

@[to_additive]
theorem eq_iff (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker :=
  by
  constructor <;> intro h
  · rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
  · rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]

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