num_le_mul_inv — Mathlib

English

The numerator I.num is contained in the product I · I^{-1} of a fractional ideal with its inverse, i.e., I.num ≤ I · I^{-1}.

Русский

Числитель I.num содержится в произведении I · I^{-1}, то есть I.num ≤ I · I^{-1}.

LaTeX

$$I.num \\le I \\cdot I^{-1}$$

Lean4

theorem num_le_mul_inv (I : FractionalIdeal R₁⁰ K) : I.num ≤ I * I⁻¹ :=
  by
  by_cases hI : I = 0
  · rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot, coeIdeal_bot]
  · rw [mul_comm, ← den_mul_self_eq_num']
    exact mul_right_mono I <| spanSingleton_le_iff_mem.2 (den_mem_inv hI)

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