isGeneratedBy_of_isFinite — Mathlib

English

If G is finite, then G is generated by the finite witness IsFinite.x.

Русский

Если G конечен, то он порождается конечным набором x, приведенным IsFinite.x.

LaTeX

$$$[hG : G.IsFinite] \Rightarrow G\text{ IsGeneratedBy }\text{IsFinite.x (G:=G)}$$$

Lean4

theorem isGeneratedBy_of_isFinite [hG : G.IsFinite] : G.IsGeneratedBy (IsFinite.x (G := G)) :=
  hG.exists_isGeneratedBy.choose_spec.choose_spec.choose_spec.choose_spec.some

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