Theorems · Definition · order theory

MonoidWithZeroHom.withTopMap

{R : Type u_2} →
  {S : Type u_3} →
    [inst : MulZeroOneClass R] →
      [inst_1 : DecidableEq R] →
        [inst_2 : Nontrivial R] →
          [inst_3 : MulZeroOneClass S] →
            [inst_4 : DecidableEq S] →
              [inst_5 : Nontrivial S] → (f : R →*₀ S) → Function.Injective ⇑f → WithTop R →*₀ WithTop S

A version of WithTop.map for MonoidWithZeroHoms.

Defined in

Mathlib.Algebra.Order.Ring.WithTop

Cited by

2 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

MulZeroOneClassDecidableEqNontrivialMulZeroOneClassDecidableEqNontrivial