divConst_inv_left

Mathlib.Combinatorics.Additive.DoublingConst

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

← MathLib Explorer

English

The δ-constant for A⁻¹ and B equals the σ-constant for A and B: δ[A⁻¹,B] = σ[A,B].

Русский

Константа δ для A⁻¹ и B равна константе σ для A и B: δ[A⁻¹,B] = σ[A,B].

LaTeX

$$\\delta[A^{-1},B] = \\sigma[A,B]$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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