card_le_card_mul_self₀ — Mathlib

English

For any Finset s in a cancellative left-multiplication semigroup with zero, |s| ≤ |s·s|.

Русский

Для любого Finset s в окружении с левым отменяемым умножением и нулём выполняется |s| ≤ |s·s|.

LaTeX

$$$|s| \le |s \cdot s|.$$$

Lean4

theorem card_le_card_mul_self₀ [IsLeftCancelMulZero α] : #s ≤ #(s * s) :=
  by
  obtain hs | hs := (s.erase 0).eq_empty_or_nonempty
  · rw [erase_eq_empty_iff] at hs
    obtain rfl | rfl := hs <;> simp
  obtain ⟨a, ha⟩ := hs
  simp only [mem_erase, ne_eq] at ha
  exact card_le_card_mul_left₀ ha.2 ha.1

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