adjoin_range_ι — Mathlib

English

The subalgebra generated by all images ι_Q(x) for x ∈ M is the entire Clifford algebra: it is top in the subalgebra lattice.

Русский

Подалгебра, генерируемая образами $ι_Q(x)$, достигает всего Clifford(Q).

LaTeX

$$$\\mathrm{Algebra.adjoin}_R\\bigl(\\mathrm{Set.range}(ι_Q)\\bigr) = \\top$$$

Lean4

@[simp]
theorem adjoin_range_ι : Algebra.adjoin R (Set.range (ι Q)) = ⊤ :=
  by
  refine top_unique fun x hx => ?_; clear hx
  induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)

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