inv_nonzero — Mathlib

English

For a nonzero I, x ∈ I^{-1} iff ∀ y ∈ I, x y ∈ 1.

Русский

Для не нулевого I выполняется: x ∈ I^{-1} тогда и только тогда, когда для всех y ∈ I верно x y ∈ 1.

LaTeX

$$$$\forall I\; (I \neq 0)\;\forall x: K,\ x \in I^{-1} \iff \forall y \in I,\ x \cdot y \in 1.$$$$

Lean4

theorem inv_nonzero {J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) :
    J⁻¹ = ⟨(1 : FractionalIdeal R₁⁰ K) / J, fractional_div_of_nonzero h⟩ :=
  div_nonzero h

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