Theorems · Definition · commutative algebra

IsLocalization.Away.tensorRightEquiv

{R : Type u_7} →
  (S : Type u_8) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (r : R) →
            (A : Type u_9) →
              [inst_3 : CommSemiring A] →
                [inst_4 : Algebra R A] →
                  [IsLocalization.Away r A] → TensorProduct R A S ≃ₐ[S] Localization.Away ((algebraMap R S) r)

The S-isomorphism S ⊗[R] Rᵣ ≃ₐ Sᵣ.

Defined in

Mathlib.RingTheory.Localization.BaseChange

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraIsLocalization.Away