card_map_of_injective — Mathlib

English

If f : G →* H is injective, then the cardinality of map f K equals card(K) for a subgroup K ≤ G.

Русский

Если f: G →* H инъективна, тоcard( map f K ) = card(K) для подгруппы K ≤ G.

LaTeX

$$$\text{If } f \text{ is injective } |\operatorname{map} f K| = |K|$$$

Lean4

@[to_additive]
theorem card_map_of_injective {H : Type*} [Group H] {K : Subgroup G} {f : G →* H} (hf : Function.Injective f) :
    Nat.card (map f K) = Nat.card K := by apply Nat.card_image_of_injective hf

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