rootForm_anisotropic — Mathlib

English

There is an instance thatP.IsAnisotropic for P when R is a linear ordered commutative ring with char zero.

Русский

Существование инстанса, устанавливающее анизотропность P при линейно упорядоченном кольце R нулевой характеристики.

LaTeX

$$P.IsAnisotropic$$

Lean4

theorem _root_.RootSystem.rootForm_anisotropic (P : RootSystem ι R M N) : P.RootForm.toQuadraticMap.Anisotropic :=
  fun x ↦
  P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero <| by
    simpa only [rootSpan, P.span_root_eq_top] using Submodule.mem_top

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