mk'_eq_zero_iff — Mathlib

English

For f: LocalizationMap S N, m ∈ M and s ∈ S, f.mk' m s = 0 if and only if there exists s' ∈ S with s' m = 0.

Русский

Для f: LocalizationMap S N, m ∈ M и s ∈ S, f.mk' m s = 0 тогда и только тогда, когда существует s' ∈ S такое, что s' m = 0.

LaTeX

$$$f.mk'\,m\,s = 0 \iff \exists s' : S, s' * m = 0$$$

Lean4

theorem mk'_eq_zero_iff (f : LocalizationMap S N) (m : M) (s : S) : f.mk' m s = 0 ↔ ∃ s : S, s * m = 0 := by
  rw [← (f.map_units s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff]

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