IsCrystallographic

Mathlib.LinearAlgebra.RootSystem.IsValuedIn

URI: https://scilib.ai/kg/mathlib#RootPairing.IsCrystallographic

← MathLib Explorer

English

A root pairing is crystallographic if every pairing is an integer.

Русский

Корневая связка кристаллизационная, если все пары значений целочисленны.

LaTeX

$$$$ \text{IsCrystallographic}(P) \iff P.IsValuedIn \mathbb{Z}. $$$$

Lean4

/-- A root pairing is said to be crystallographic if the pairing between a root and coroot is
always an integer. -/
abbrev IsCrystallographic :=
  P.IsValuedIn ℤ

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

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

Разделы

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

Аффилиация

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