card_le_card_div_left — Mathlib

English

For a finite nonempty S in a group, the left quotient S / T has cardinality at least as large as |T|, i.e., |T| ≤ |S / T|.

Русский

Для конечного непустого S в группе множество левых делений S / T имеет кардинальность не меньше, чем |T|, то есть |T| ≤ |S / T|.

LaTeX

$$$s.Nonempty \Rightarrow |t| \le |s / t|$$$

Lean4

@[to_additive]
theorem card_le_card_div_left (hs : s.Nonempty) : #t ≤ #(s / t) :=
  have ⟨_, ha⟩ := hs;
  card_le_card_image₂_left _ ha div_right_injective

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