eq_one_div_of_mul_eq_one_right — Mathlib

English

If I and J satisfy I ⋅ J = 1, then J = 1 / I. In particular, J is the inverse of I.

Русский

Если произведение I и J равно единице, то J = 1 / I. Соответственно, J — обратный к I.

LaTeX

$$$ I \cdot J = 1 \quad\Longrightarrow\quad J = 1 / I $$$

Lean4

theorem eq_one_div_of_mul_eq_one_right (I J : FractionalIdeal R₁⁰ K) (h : I * J = 1) : J = 1 / I :=
  by
  have hI : I ≠ 0 := ne_zero_of_mul_eq_one I J h
  suffices h' : I * (1 / I) = 1 from
    congr_arg Units.inv <| @Units.ext _ _ (Units.mkOfMulEqOne _ _ h) (Units.mkOfMulEqOne _ _ h') rfl
  apply le_antisymm
  · apply mul_le.mpr _
    intro x hx y hy
    rw [mul_comm]
    exact (mem_div_iff_of_nonzero hI).mp hy x hx
  rw [← h]
  apply mul_left_mono I
  apply (le_div_iff_of_nonzero hI).mpr _
  intro y hy x hx
  rw [mul_comm]
  exact mul_mem_mul hy hx

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