mulConst_inv_right

Mathlib.Combinatorics.Additive.DoublingConst

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

English

Replacing B by B^{-1} converts the span to a difference constant: σ_m[A,B^{-1}] = δ_m[A,B].

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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