bot_lt_mul_inv — Mathlib

English

If I is a nonzero fractional ideal, then the product I · I^{-1} is strictly greater than the bottom element (nontriviality of the inverse product).

Русский

Если I ≠ 0, то I · I^{-1} превосходит минимальный элемент, т.е. не равно ⊥.

LaTeX

$$⊥ < I \\cdot I^{-1} \\quad \\text{whenever } I \\neq ⊥$$

Lean4

theorem bot_lt_mul_inv {I : FractionalIdeal R₁⁰ K} (hI : I ≠ ⊥) : ⊥ < I * I⁻¹ :=
  lt_of_lt_of_le (coeIdeal_ne_zero.2 (hI ∘ num_eq_zero_iff.1)).bot_lt I.num_le_mul_inv

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