adjoin_union_eq_adjoin_adjoin — Mathlib

English

The algebra generated by the union s ∪ t over R equals the scalars-restriction of the algebra generated by t over the algebra generated by s: adjoin_R(s ∪ t) = (adjoin(adjoin_R s) t).restrictScalars R.

Русский

Алгебра, порождаемая объединением s ∪ t над R, равна ограничению по скалярам алгебры, порождаемой t над алгеброй, порожденной s: adjoin_R(s ∪ t) = (adjoin(adjoin_R s) t).restrictScalars R.

LaTeX

$$$\\operatorname{adjoin}_R(s \\cup t) = (\\operatorname{adjoin}(\\operatorname{adjoin}_R s)\\; t)\\text{.restrictScalars}_R$$$

Lean4

theorem adjoin_union_eq_adjoin_adjoin : adjoin R (s ∪ t) = (adjoin (adjoin R s) t).restrictScalars R := by
  simpa using adjoin_algebraMap_image_union_eq_adjoin_adjoin R s t

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