divConst_inv_right

Mathlib.Combinatorics.Additive.DoublingConst

URI: https://scilib.ai/kg/mathlib#Finset.divConst_inv_right

English

Replacing B by B^{-1} equates the difference and doubling constants: δ_m[A,B^{-1}] = σ_m[A,B].

Русский

Замена B на B^{-1} превращает разностную константу в удвоенную: δ_m[A,B^{-1}] = σ_m[A,B].

LaTeX

$$$\delta_m[A,B^{-1}] = \sigma_m[A,B]$$$

Lean4

@[to_additive (attr := simp)]
theorem divConst_inv_right (A B : Finset G) : δₘ[A, B⁻¹] = σₘ[A, B] := by rw [mulConst, divConst, div_inv_eq_mul]

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

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

Разделы

Аффилиация

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