instIsAnisotropicFlip — Mathlib

English

If P is a finite crystallographic root pairing, then the flip of P inherits anisotropy: P.flip.IsAnisotropic whenever P.IsAnisotropic.

Русский

Если P — конечная кристаллографическая корневая пара, то анизотропия сохраняется под разворотом: P.flip.IsAnisotropic если P.IsAnisotropic.

LaTeX

$$[P.IsAnisotropic] ⇒ P.flip.IsAnisotropic$$

Lean4

instance [P.IsAnisotropic] : P.flip.IsAnisotropic
    where
  rootForm_root_ne_zero := IsAnisotropic.corootForm_coroot_ne_zero
  corootForm_coroot_ne_zero := IsAnisotropic.rootForm_root_ne_zero (P := P)

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