instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan

English

There exists a finite type of elements for the extended independent set in the division ring context, ensuring a finite extension step in the induction on rank.

Русский

Существует конечный тип элементов для расширенного независимого множества в контексте деления кольца, обеспечивая конечный шаг расширения в индукции по рангу.

LaTeX

$$Nonempty (Fintype (hs.extend hst).Elem)$$

Lean4

noncomputable instance {R M : Type*} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set M}
    [Module.Finite R (span R t)] (hs : LinearIndepOn R id s) (hst : s ⊆ t) : Fintype (hs.extend hst) :=
  by
  refine Classical.choice (Cardinal.lt_aleph0_iff_fintype.1 ?_)
  rw [← rank_span_set (hs.linearIndepOn_extend hst), hs.span_extend_eq_span]
  exact Module.rank_lt_aleph0 ..

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