Theorems · Definition · ring theory

NonUnitalSubring.comap

{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 S → NonUnitalSubring R

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

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

15 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRingFunLikeNonUnitalRingHomClass