Theorems · Theorem · commutative algebra

ClassGroup.extendedHom_mk

∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDomain A] [inst_5 : IsDomain B]
  (I : (FractionalIdeal (nonZeroDivisors A) (FractionRing A))ˣ),
  (ClassGroup.extendedHom A B) ((ClassGroup.mk (FractionRing A)) I) =
    (ClassGroup.mk (FractionRing B)) ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) I)

Defined in

Mathlib.RingTheory.ClassGroup.ExtendedHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraModule.IsTorsionFreeIsDomainIsDomain