mk_mem_cotangentIdeal — Mathlib

English

For x ∈ R, Quotient.mk(I^2) x ∈ I.cotangentIdeal iff x ∈ I.

Русский

Для x ∈ R: Quotient.mk(I^2) x ∈ I.cotangentIdeal ↔ x ∈ I.

LaTeX

$$$\\text{Quotient.mk}(I^2)\\,x \\in I.cotangentIdeal \\iff x \\in I$$$

Lean4

theorem mk_mem_cotangentIdeal {I : Ideal R} {x : R} : Quotient.mk (I ^ 2) x ∈ I.cotangentIdeal ↔ x ∈ I :=
  by
  refine ⟨fun ⟨y, hy, e⟩ ↦ ?_, fun h ↦ ⟨x, h, rfl⟩⟩
  simpa using sub_mem hy (Ideal.pow_le_self two_ne_zero ((Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp e))

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