compl_beattySeq'

Mathlib.NumberTheory.Rayleigh

URI: https://scilib.ai/kg/mathlib#compl_beattySeq'

← MathLib Explorer

English

For p maximal and IsGalois, inertiaDegIn p B = inertiaDeg p P.

Русский

Для максимального p и IsGalois, inertiaDegIn p B = inertiaDeg p P.

LaTeX

$$$\\mathrm{inertiaDegIn}\\ p\\ B = \\mathrm{inertiaDeg}\\ p\\ P$$$

Lean4

theorem compl_beattySeq' {r s : ℝ} (hrs : r.HolderConjugate s) : {beattySeq' r k | k}ᶜ = {beattySeq s k | k} := by
  rw [← compl_beattySeq hrs.symm, compl_compl]

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

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

Разделы

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

Аффилиация

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