Theorems · Definition · ring theory

NonUnitalSubring.map

{F : Type w} →
  {R : Type u} →
    {S : Type v} →
      [inst : NonUnitalNonAssocRing R] →
        [inst_1 : NonUnitalNonAssocRing S] →
          [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSubring R → NonUnitalSubring S

The image of a NonUnitalSubring along a ring homomorphism is a NonUnitalSubring.

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

19 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRingFunLikeNonUnitalRingHomClass