Theorems · Definition · number theory

NumberField.RingOfIntegers.mapRingEquiv

{K : Type u_3} →
  {L : Type u_4} →
    [inst : Field K] → [inst_1 : Field L] → K ≃+* L → NumberField.RingOfIntegers K ≃+* NumberField.RingOfIntegers L

The ring isomorphism (𝓞 K) ≃+* (𝓞 L) given by restricting a ring isomorphism e : K ≃+* L to 𝓞 K.

Defined in

Mathlib.NumberTheory.NumberField.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldField