adjoin_eq_range_algebraMap_adjoin

English

The underlying set of adjoin F S in E equals the range of the algebra map from adjoin F S to E.

Русский

Множество adjoin F S как подполе E равно образу алгебраической карты из adjoin F S в E.

LaTeX

$$$\operatorname{range}(\mathrm{algebraMap}(\operatorname{adjoin} F S, E)) = \operatorname{adjoin}_F S$$$

Lean4

theorem adjoin_eq_range_algebraMap_adjoin : (adjoin F S : Set E) = Set.range (algebraMap (adjoin F S) E) :=
  Subtype.range_coe.symm

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