cast_addConst — Mathlib

English

Let A,B be finite subsets of a target group G'. Then the field-valued quantity σ[A,B] equals the ratio of the sizes of A+B to A: (σ[A,B] : 𝕜) = |A+B|/|A|.

Русский

Пусть A,B — конечные подмножества группы G'. Тогда скалярная величина σ[A,B] равна отношению размера сферы суммы A+B к |A|: (σ[A,B] : 𝕜) = |A+B|/|A|.

LaTeX

$$$\\sigma[A,B] = \\dfrac{|A+B|}{|A|}$$$

Lean4

theorem cast_addConst (A B : Finset G') : (σ[A, B] : 𝕜) = #(A + B) / #A := by simp [addConst]

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