∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B],
  ValuativeExtension.mapValueGroupWithZero A B =
    ValuativeRel.ValueGroupWithZero.embed (Valuation.comap (algebraMap A B) (ValuativeRel.valuation B))