Theorems · Definition · commutative algebra

WithIdeal.uniformEquiv

{R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : WithIdeal R] →
      {S : Type u_2} →
        [inst_2 : CommRing S] →
          [inst_3 : WithIdeal S] → (e : R ≃+* S) → Ideal.map e.toRingHom WithIdeal.i = WithIdeal.i → R ≃ᵤ S

A ring equivalence induces a uniform equivalence with respect to the adic topologies, provided it preserves the defining ideals.

Defined in

Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Cited by

3 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingWithIdealCommRingWithIdeal