apply_mem_of_equiv_iff — Mathlib

English

Let f: R ≃+* S be a ring equivalence and I an ideal of R. For x ∈ R the membership f(x) ∈ I.map f is equivalent to x ∈ I.

Русский

Пусть f: R ≃+* S — кольцевая эквивалентность. Тогда для любого x ∈ R: f(x) ∈ I.map f эквивалентно x ∈ I.

LaTeX

$$$f(x) \\in I.map f \\;\\iff\\; x \\in I$$$

Lean4

@[simp]
theorem apply_mem_of_equiv_iff {I : Ideal R} {f : R ≃+* S} {x : R} : f x ∈ I.map f ↔ x ∈ I := by
  rw [← comap_symm, Ideal.mem_comap, f.symm_apply_apply]

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