le_self_mul_one_div — Mathlib

English

If I,J are fractional with J ≠ 0, then instHDiv.hDiv I.coeToSubmodule J.coeToSubmodule is fractional.

Русский

Если I,J дробные и J ≠ 0, то instHDiv.hDiv I.coeToSubmodule J.coeToSubmodule дробный.

LaTeX

$$IsFractional (nonZeroDivisors R₁) (instHDiv.hDiv I.coeToSubmodule J.coeToSubmodule)$$

Lean4

theorem le_self_mul_one_div {I : FractionalIdeal R₁⁰ K} (hI : I ≤ (1 : FractionalIdeal R₁⁰ K)) : I ≤ I * (1 / I) :=
  by
  by_cases hI_nz : I = 0
  · rw [hI_nz, div_zero, mul_zero]
  · rw [← coe_le_coe, coe_mul, coe_div hI_nz, coe_one]
    rw [← coe_le_coe, coe_one] at hI
    exact Submodule.le_self_mul_one_div hI

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