ncard_dvd_card — Mathlib

English

If B is a nonempty block for a group action of G on X (with IsPretransitive), then the number of elements of B divides the number of elements of X.

Русский

Пусть B — непустый блок действия группы G на X (при условии, что действие преразмерено/pretransitive). Тогда кардинал B делит кардинал X.

LaTeX

$$$\operatorname{Set.ncard}(B) \mid \operatorname{Nat.card}(X)$$$

Lean4

/-- The cardinality of a block divides the cardinality of the ambient type -/
@[to_additive /-- The cardinality of a block divides the cardinality of the ambient type -/
    ]
theorem ncard_dvd_card (hB : IsBlock G B) (hB_ne : B.Nonempty) : Set.ncard B ∣ Nat.card X :=
  Dvd.intro _ (hB.ncard_block_mul_ncard_orbit_eq hB_ne)

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