idealOfLE_ofPrime — Mathlib

English

The ideal obtained by idealOfLE with respect to A.ofPrime P equals P.

Русский

Идеал, полученный через idealOfLE по A.ofPrime P, равен P.

LaTeX

$$idealOfLE A (A.ofPrime P) (le_ofPrime A P) = P$$

Lean4

@[simp]
theorem idealOfLE_ofPrime (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
    idealOfLE A (ofPrime A P) (le_ofPrime A P) = P :=
  by
  refine Ideal.ext (fun x => ?_)
  apply IsLocalization.AtPrime.to_map_mem_maximal_iff
  exact isLocalRing (ofPrime A P)

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