adjoin_gen_eq_top — Mathlib

English

The subalgebra generated by a single element B.gen is the whole algebra, i.e., adjoin R({B.gen}) = ⊤.

Русский

Образующаяся подалгебра из одного элемента B.gen равна всей алгебре: adjoin R({B.gen}) = ⊤.

LaTeX

$$$ adjoin\ R\ (\{ B.gen \} : Set S) = \top $$$

Lean4

theorem adjoin_gen_eq_top (B : PowerBasis R S) : adjoin R ({ B.gen } : Set S) = ⊤ :=
  by
  rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]
  rintro x ⟨i, rfl⟩
  rw [B.basis_eq_pow i]
  exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

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