natCard_smul_set₀

Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.natCard_smul_set₀

English

If a ≠ 0 acts on a set s, then the natural cardinality of a·s equals the natural cardinality of s.

Русский

Если a ≠ 0 действует на множество s, то Nat.card(a·s) = Nat.card(s).

LaTeX

$$$\mathrm{Nat.card} (a \cdot s) = \mathrm{Nat.card} (s)$$$

Lean4

theorem natCard_smul_set₀ (ha : a ≠ 0) (s : Set M₀) : Nat.card ↥(a • s) = Nat.card s :=
  Nat.card_image_of_injective (MulAction.injective₀ ha) _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru