Theorems · Theorem · commutative algebra

CommRing.Pic.mapAlgebra_mapAlgebra

∀ {R : Type u} [inst : CommSemiring R] {A : Type u_5} {B : Type u_6} [inst_1 : CommSemiring A] [inst_2 : CommSemiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] {M : CommRing.Pic R},
  (CommRing.Pic.mapAlgebra A B) ((CommRing.Pic.mapAlgebra R A) M) = (CommRing.Pic.mapAlgebra R B) M

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringAlgebraAlgebraAlgebraIsScalarTower