instIsValuedInFlip — Mathlib

English

Equivalently stated for the flipped pairing: P.IsValuedIn S iff root-pairings lie in the range of the algebra map.

Русский

Эквивалентно для перевернутой пары: P.IsValuedIn S эквивалентно принадлежности корневых пар к диапазону алгебраобразования.

LaTeX

$$$$ P.IsValuedIn S \iff \forall i,j, P.pairing i j \in \mathrm{range}(\text{algebraMap } S R). $$$$

Lean4

instance [P.IsValuedIn S] : P.flip.IsValuedIn S :=
  by
  rw [isValuedIn_iff, forall_comm]
  exact P.exists_value

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