Theorems · Theorem · commutative algebra

Algebra.adjoin_top

∀ (R : Type uR) {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra S A] (t : Set A),
  Algebra.adjoin (↥⊤) t = Subalgebra.restrictScalars (↥⊤) (Algebra.adjoin S t)

Defined in

Mathlib.RingTheory.Adjoin.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraSemiringAlgebra