mk'_eq_zero_iff_eq_zero — Mathlib

English

For any x ∈ R and y ∈ nonZeroDivisors(R), mk' K x y = 0 if and only if x = 0.

Русский

При любом x ∈ R и y ∈ nonZeroDivisors(R), mk' K x y = 0 тогда и только тогда, когда x = 0.

LaTeX

$$mk'_eq_zero_iff_eq_zero {x} {y} : mk' K x y = 0 ↔ x = 0$$

Lean4

theorem mk'_eq_zero_iff_eq_zero [Algebra R K] [IsFractionRing R K] {x : R} {y : nonZeroDivisors R} :
    mk' K x y = 0 ↔ x = 0 := by
  haveI := (algebraMap R K).domain_nontrivial
  simp [nonZeroDivisors.ne_zero]

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