Theorems · Theorem · ring theory

NonUnitalSubring.map_le_iff_le_comap

∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f : F} {s : NonUnitalSubring R}
  {t : NonUnitalSubring S}, NonUnitalSubring.map f s ≤ t ↔ s ≤ NonUnitalSubring.comap f t

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

1 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRingFunLikeNonUnitalRingHomClass