denom_notMem — Mathlib

English

The element f does not belong to the ideal I = carrier.asIdeal f_deg hm q.

Русский

Элемент f не принадлежит идеалу I = carrier.asIdeal f_deg hm q.

LaTeX

$$$f \notin carrier.asIdeal f_{deg} hm q$$$

Lean4

theorem denom_notMem : f ∉ carrier.asIdeal f_deg hm q := fun rid =>
  q.isPrime.ne_top <|
    (Ideal.eq_top_iff_one _).mpr
      (by
        convert rid m
        rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_one, HomogeneousLocalization.val_mk]
        dsimp
        simp_rw [decompose_of_mem_same _ f_deg]
        simp only [mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self])

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