restrictScalars_adjoin — Mathlib

English

For F ⟨CommSemiring⟩ and E with algebra F E, the restriction of scalars of adjoin_K S equals adjoin_F (K ∪ S).

Русский

Для F ⟨комм-кольца⟩ и E с алгеброй F E выполнено: (adjoin_K S).restrictScalars F = adjoin_F (K ∪ S).

LaTeX

$$$\\operatorname{restrictScalars}_F(\\operatorname{adjoin}_K S) = \\operatorname{adjoin}_F (K \\cup S)$$

Lean4

theorem restrictScalars_adjoin (F : Type*) [CommSemiring F] {E : Type*} [CommSemiring E] [Algebra F E]
    (K : Subalgebra F E) (S : Set E) : (Algebra.adjoin K S).restrictScalars F = Algebra.adjoin F (K ∪ S) := by
  conv_lhs => rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]

Похожие утверждения