le_dual_inv_aux — Mathlib

English

If I ≠ 0 and I J ≤ 1, then J ≤ dual A K I.

Русский

Если I ≠ 0 и I J ≤ 1, тогда J ≤ dual A K I.

LaTeX

$$le_dual_inv_aux : (hI : I ≠ 0) (hIJ : I * J ≤ 1) → J ≤ dual A K I.$$

Lean4

theorem le_dual_inv_aux (hI : I ≠ 0) (hIJ : I * J ≤ 1) : J ≤ dual A K I :=
  by
  rw [dual, dif_neg hI]
  intro x hx y hy
  rw [mem_one]
  apply IsIntegrallyClosed.isIntegral_iff.mp
  apply isIntegral_trace
  rw [IsIntegralClosure.isIntegral_iff (A := B)]
  have ⟨z, _, hz⟩ := hIJ (FractionalIdeal.mul_mem_mul hy hx)
  rw [mul_comm] at hz
  exact ⟨z, hz⟩

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