admissible_E'5

Mathlib.NumberTheory.ADEInequality

URI: https://scilib.ai/kg/mathlib#ADEInequality.admissible_E'5

English

Admissible(E' 5). The triple E'5 is admissible.

Русский

Admissible(E' 5). Тройка E'5 допустима.

LaTeX

$$$\operatorname{Admissible}(E'_5)$$$

Lean4

theorem admissible_E'5 : Admissible (E' 5) :=
  Or.inr <| Or.inr <| Or.inr <| Or.inr rfl

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

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

Разделы

Аффилиация

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