nnratCast_dens — Mathlib

English

The density of s, viewed as an element of the field 𝕜, equals card(s) divided by card(α).

Русский

Плотность s, рассматриваемая как элемент поля 𝕜, равна отношению card(s) к card(α).

LaTeX

$$$ (\\operatorname{dens}(s) : \\mathbb{𝕜}) = \\dfrac{\\operatorname{card}(s)}{\\operatorname{card}(\\alpha)} $$$

Lean4

@[norm_cast]
theorem nnratCast_dens (s : Finset α) : (s.dens : 𝕜) = s.card / Fintype.card α := by simp [dens]

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