Theorems · Definition · commutative algebra

FractionalIdeal.mapEquiv

{R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            {P' : Type u_3} →
              [inst_3 : CommRing P'] →
                [inst_4 : Algebra R P'] → (P ≃ₐ[R] P') → FractionalIdeal S P ≃+* FractionalIdeal S P'

If g is an equivalence, map g is an isomorphism

Defined in

Mathlib.RingTheory.FractionalIdeal.Operations

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebra