cast_divConst — Mathlib

English

For finite A,B in G, the constant δ[A,B] cast to 𝕜 equals the ratio |A/B|/|A|, where A/B is the quotient/difference operation in the ambient structure.

Русский

Для конечных A,B в группе G константа δ[A,B], приведенная в 𝕜, равна отношению |A/B| к |A|.

LaTeX

$$$\\delta[A,B] = \\dfrac{|A/B|}{|A|}$$$

Lean4

theorem cast_divConst (A B : Finset G) : (δₘ[A, B] : 𝕜) = #(A / B) / #A := by simp [divConst]

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