one_mem_inv_coe_ideal — Mathlib

English

If I is a nonzero ideal of A, then 1 lies in the inverse of I when viewed as a fractional ideal.

Русский

Если I не нулевой идеал A, то 1 принадлежит I^{-1} как дробному идеалу.

LaTeX

$$$$I \\neq \\perp \\;\\Rightarrow\\; 1 \\in (I)^{-1}.$$$$

Lean4

theorem one_mem_inv_coe_ideal [IsDomain A] {I : Ideal A} (hI : I ≠ ⊥) : (1 : K) ∈ (I : FractionalIdeal A⁰ K)⁻¹ :=
  by
  rw [FractionalIdeal.mem_inv_iff (FractionalIdeal.coeIdeal_ne_zero.mpr hI)]
  intro y hy
  rw [one_mul]
  exact FractionalIdeal.coeIdeal_le_one hy

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