toInvariantForm — Mathlib

English

If B and B_1 are RootPositiveForm for the same P and B = B_1, then their associated invariant forms coincide after forgetting positivity data.

Русский

Если B и B_1 — RootPositiveForm для одного и того же P и B = B_1, то их соответствующие инвариантные формы совпадают после удаления данных о положительности.

LaTeX

$$$ B = B_1 \\Rightarrow B.toInvariantForm = B_1.toInvariantForm $$$

Lean4

/-- Forgetting the positivity condition, we may regard a `RootPositiveForm` as an `InvariantForm`.
-/
@[simps]
def toInvariantForm : InvariantForm P where
  form := B.form
  symm := B.symm
  ne_zero := B.form_apply_root_ne_zero
  isOrthogonal_reflection := B.isOrthogonal_reflection

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