Theorems · Theorem · commutative algebra

Subsemiring.map_iInf

∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {ι : Sort u_1} [Nonempty ι]
  (f : R →+* S),
  Function.Injective ⇑f → ∀ (s : ι → Subsemiring R), Subsemiring.map f (iInf s) = ⨅ i, Subsemiring.map f (s i)

Defined in

Mathlib.Algebra.Ring.Subsemiring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiringNonempty