Theorems · Definition · commutative algebra

ValuativeExtension.mapValueGroupWithZero

(A : Type u_1) →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : Ring B] →
        [inst_2 : ValuativeRel A] →
          [inst_3 : ValuativeRel B] →
            [inst_4 : Algebra A B] →
              [ValuativeExtension A B] → ValuativeRel.ValueGroupWithZero A →*₀ ValuativeRel.ValueGroupWithZero B

The map on value groups-with-zero associated to the structure morphism of an algebra.

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingRingValuativeRelValuativeRelAlgebraValuativeExtension