toENat_rank_span_set — Mathlib

English

An induction principle for all submodules of a fixed finite free module M: if a property P holds for submodules N with the stated inductive step, then P holds for all submodules of M.

Русский

Индуктивный принцип для всех подмодулов фиксированного конечного свободного модуля M: если свойство P удовлетворяет указанному шагу индукции, то P поддерживается для всех подмодулов M.

LaTeX

$$$\\text{Submodule.inductionOnRank}(b, P)$$$

Lean4

theorem toENat_rank_span_set {v : ι → M} {s : Set ι} (hs : LinearIndepOn R v s) :
    (Module.rank R <| span R <| v '' s).toENat = s.encard := by
  rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range, ← rank_span hs.linearIndependent]

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