mk'_mem_iff — Mathlib

English

Membership of the localized element to an ideal is equivalent to membership of its image under algebraMap.

Русский

Членство локализованного элемента в идеале эквивалентно членству его образа под algebraMap.

LaTeX

$$mk'_mem_iff S x y I$$

Lean4

theorem mk'_mem_iff {x} {y : M} {I : Ideal S} : mk' S x y ∈ I ↔ algebraMap R S x ∈ I :=
  by
  constructor <;> intro h
  · rw [← mk'_spec S x y, mul_comm]
    exact I.mul_mem_left ((algebraMap R S) y) h
  · rw [← mk'_spec S x y] at h
    obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (map_units S y)
    have := I.mul_mem_left b h
    rwa [mul_comm, mul_assoc, hb, mul_one] at this

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