isLocalRing — Mathlib

English

If a ring is local, then any ring equivalence with another ring preserves locality.

Русский

Если кольцо локально, то любое кольцевое эквивалентное кольцо также локально.

LaTeX

$$$\forall e:\ A \simeq+^* B,\; \text{IsLocalRing } A \Rightarrow \text{IsLocalRing } B$$$

Lean4

protected theorem isLocalRing {A B : Type*} [CommSemiring A] [IsLocalRing A] [Semiring B] (e : A ≃+* B) :
    IsLocalRing B :=
  haveI := e.symm.toEquiv.nontrivial
  IsLocalRing.of_surjective (e : A →+* B) e.surjective

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