Theorems · Theorem · ring theory

Subalgebra.pi_mono

∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] {s : Set ι} {t₁ t₂ : (i : ι) → Subalgebra R (S i)},
  (∀ i ∈ s, t₁ i ≤ t₂ i) → Subalgebra.pi s t₁ ≤ Subalgebra.pi s t₂

Defined in

Mathlib.Algebra.Algebra.Subalgebra.Pi

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra