isFixedPt_reflectionPerm_iff — Mathlib

English

Let i and j be indices in ι. Under the same hypotheses as above, IsFixedPt (P.reflectionPerm i) j holds if and only if P.pairing i j = 0.

Русский

Пусть i и j — элементы ι. При тех же предположениях верно: IsFixedPt (P.reflectionPerm i) j ⇔ P.pairing i j = 0.

LaTeX

$$$ \\text{IsFixedPt}(P.reflectionPerm(i), j) \\iff P.pairing(i,j) = 0 $$$

Lean4

theorem isFixedPt_reflectionPerm_iff [NeZero (2 : R)] [NoZeroSMulDivisors R M] :
    IsFixedPt (P.reflectionPerm i) j ↔ P.pairing i j = 0 :=
  by
  refine ⟨fun h ↦ ?_, P.reflectionPerm_eq_of_pairing_eq_zero'⟩
  simpa [P.ne_zero i, pairing_eq_zero_iff, IsFixedPt, reflectionPerm_eq_iff_smul_root] using h

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