eq_zero_of_fst_eq_zero — Mathlib

English

If z·f(y) = f(x) and f(x) = 0 with x ∈ R, then z = 0.

Русский

Если $z\\cdot f(y) = f(x)$ и $f(x)=0$, то $z=0$.

LaTeX

$$$z\\cdot\\varphi(y) = \\varphi(x) \\quad\\text{and } x=0 \\Rightarrow z=0$, with $\\varphi = \\text{algebraMap } R S$$$

Lean4

theorem eq_zero_of_fst_eq_zero {z x} {y : M} (h : z * algebraMap R S y = algebraMap R S x) (hx : x = 0) : z = 0 :=
  by
  rw [hx, (algebraMap R S).map_zero] at h
  exact (IsUnit.mul_left_eq_zero (IsLocalization.map_units S y)).1 h

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