Theorems · Definition · Lie groups

AbsoluteValue.comp

{R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Semiring T] →
        [inst_1 : Semiring R] →
          [inst_2 : Semiring S] →
            [inst_3 : PartialOrder S] → AbsoluteValue R S → {f : T →+* R} → Function.Injective ⇑f → AbsoluteValue T S

Construct an absolute value on a semiring T from an absolute value on a semiring R and an injective ring homomorphism f : T →+* R

Defined in

Mathlib.Topology.Algebra.Ring.Basic

Cited by

3 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

SemiringSemiringSemiringPartialOrder