mulEnergy_univ_right

Mathlib.Combinatorics.Additive.Energy

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

English

The multiplicative energy is symmetric in its two arguments: E_m[s,t] = E_m[t,s].

Русский

Мультипликативная энергия симметрична по отношению к аргументам: E_m[s,t] = E_m[t,s].

LaTeX

$$E_m[s,t] = E_m[t,s]$$

Lean4

@[to_additive (attr := simp)]
theorem mulEnergy_univ_right : Eₘ[s, univ] = Fintype.card α * s.card ^ 2 := by rw [mulEnergy_comm, mulEnergy_univ_left]

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

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

Разделы

Аффилиация

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