rank_le — Mathlib

English

If S is a finite subset of G generating G (i.e. ⟨S⟩ = G), then rank(G) ≤ |S|.

Русский

Если S является конечным подмножеством G, порождающим G (то есть ⟨S⟩ = G), то rank(G) ≤ |S|.

LaTeX

$$$\forall S \subseteq G\ (\text{finite})\ [\langle S \rangle = G] \Rightarrow \operatorname{rank}(G) \le |S|.$$$

Lean4

@[to_additive]
theorem rank_le [h : FG G] {S : Finset G} (hS : .closure S = (⊤ : Subgroup G)) : rank G ≤ S.card :=
  @Nat.find_le _ _ (Classical.decPred _) (fg_iff'.mp h) ⟨S, rfl, hS⟩

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