instIsAnisotropicOfIsCrystallographic

English

Every crystallographic root pairing P is anisotropic in the sense of its root form if the base ring is characteristic zero; more precisely, there is an instance IsAnisotropic P when P.IsCrystallographic.

Русский

Каждая кристаллографическая корневая пара P является анизотропной в смысле её корневой формы при нулевой характеристики базового кольца; существует экземпляр IsAnisotropic P, если P IsCrystallographic.

LaTeX

$$[P.IsCrystallographic] ⇒ IsAnisotropic P$$

Lean4

instance instIsAnisotropicOfIsCrystallographic [CharZero R] [P.IsCrystallographic] : IsAnisotropic P :=
  P.isAnisotropic_of_isValuedIn ℤ

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