Theorems · Theorem · commutative algebra

RingHom.rangeS_codRestrict

∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σS : Type u_2}
  [inst_2 : SetLike σS S] [inst_3 : SubsemiringClass σS S] {f : R →+* S} {s : σS} {h : ∀ (x : R), f x ∈ s},
  (f.codRestrict s h).rangeS = Subsemiring.comap (SubsemiringClass.subtype s) f.rangeS

Defined in

Mathlib.Algebra.Ring.Subsemiring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiringSetLikeSubsemiringClass