mk'_eq_one_iff_eq — Mathlib

English

For any x ∈ A and y ∈ nonZeroDivisors(A), mk' K x y = 1 if and only if x equals y (in the fraction sense).

Русский

Для любых x ∈ A и y ∈ nonZeroDivisors(A), mk' K x y = 1 тогда, когда x равно y в дробной локализации.

LaTeX

$$mk'_eq_one_iff_eq {x} {y} : mk' K x y = 1 ↔ x = y$$

Lean4

theorem mk'_eq_one_iff_eq {x : A} {y : nonZeroDivisors A} : mk' K x y = 1 ↔ x = y :=
  by
  haveI := (algebraMap A K).domain_nontrivial
  refine ⟨?_, fun hxy => by rw [hxy, mk'_self']⟩
  intro hxy
  have hy : (algebraMap A K) ↑y ≠ (0 : K) := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property
  rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy
  exact IsFractionRing.injective A K hxy

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