unramifiedLocus — Mathlib

English

Define the unramified locus of primes in A as those where IsUnramifiedAt R p.asIdeal holds.

Русский

Определим множество локуса неразветвленности как множества простых идеалов p в A, удовлетворяющих IsUnramifiedAt R p.asIdeal.

LaTeX

$$unramifiedLocus(R,A) = { p ∈ PrimeSpectrum A | IsUnramifiedAt R p.asIdeal }$$

Lean4

/-- `Algebra.unramifiedLocus R A` is the set of primes `p` of `A` that are unramified. -/
def unramifiedLocus : Set (PrimeSpectrum A) :=
  {p | IsUnramifiedAt R p.asIdeal}

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