numeratorHom_inj — Mathlib

English

If S is contained in the left nonzero divisors of R, then the numerator map numeratorHom: R → R[S⁻¹] is injective.

Русский

Если S ⊆ левых ненулевых делителей R, то отображение numeratorHom: R → R[S⁻¹] инъективно.

LaTeX

$$If $S \\le \\mathrm{nonZeroDivisorsLeft}(R)$ then the map \$\\mathrm{numeratorHom}: R \\to R[S^{-1}]\$ is injective.$$

Lean4

theorem numeratorHom_inj (hS : S ≤ nonZeroDivisorsLeft R) : Function.Injective (numeratorHom : R → R[S⁻¹]) :=
  fun r₁ r₂ h => by
  rw [numeratorHom_apply, numeratorHom_apply, oreDiv_eq_iff] at h
  rcases h with ⟨u, v, h₁, h₂⟩
  simp only [S.coe_one, mul_one, Submonoid.smul_def, smul_eq_mul] at h₁ h₂
  rw [← h₂, ← sub_eq_zero, ← mul_sub] at h₁
  exact (sub_eq_zero.mp (hS u.2 _ h₁)).symm

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