Theorems · Theorem · ring theory

NonUnitalRingHom.closure_preimage_le

∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S)
  (s : Set S), NonUnitalSubring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubring.comap f (NonUnitalSubring.closure s)

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRing