eq_zero_or_one — Mathlib

English

For any isomorphism h, the image of 1 / I equals 1 / (I.map h).

Русский

Для любого изоморфизма h образ 1 / I равен 1 / (I.map h).

LaTeX

$$$ (1 / I) map\ h = 1 / (I map\ h) $$$

Lean4

theorem eq_zero_or_one (I : FractionalIdeal K⁰ L) : I = 0 ∨ I = 1 :=
  by
  rw [or_iff_not_imp_left]
  intro hI
  simp_rw [@SetLike.ext_iff _ _ _ I 1, mem_one_iff]
  intro x
  constructor
  · intro x_mem
    obtain ⟨n, d, rfl⟩ := IsLocalization.mk'_surjective K⁰ x
    refine ⟨n / d, ?_⟩
    rw [map_div₀, IsFractionRing.mk'_eq_div]
  · rintro ⟨x, rfl⟩
    obtain ⟨y, y_ne, y_mem⟩ := exists_ne_zero_mem_isInteger hI
    rw [← div_mul_cancel₀ x y_ne, RingHom.map_mul, ← Algebra.smul_def]
    exact smul_mem (M := L) I (x / y) y_mem

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