neg_mem' — Mathlib

English

Product of two locally fractional sections is locally fractional; the sections form a subring under multiplication.

Русский

Произведение двух локально дробных секций локально дробно; секции образуют подпольцо относительно умножения.

LaTeX

$$$$a\cdot b \in \text{sectionsSubring}(U)$$$$

Lean4

theorem neg_mem' (U : (Opens (ProjectiveSpectrum.top 𝒜))ᵒᵖ) (a : ∀ x : U.unop, at x.1)
    (ha : (isLocallyFraction 𝒜).pred a) : (isLocallyFraction 𝒜).pred (-a) := fun x =>
  by
  rcases ha x with ⟨V, m, i, j, ⟨r, r_mem⟩, ⟨s, s_mem⟩, nin, hy⟩
  refine ⟨V, m, i, j, ⟨-r, Submodule.neg_mem _ r_mem⟩, ⟨s, s_mem⟩, nin, fun y => ?_⟩
  simp only [ext_iff_val, val_mk] at hy
  simp only [Pi.neg_apply, ext_iff_val, val_neg, hy, val_mk, neg_mk]

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