toPerfPair_conj_reflection — Mathlib

English

The conjugation in the perf-pairing of a reflection equals the dual map of the corresponding coreflection, i.e., conj of reflection equals the dual map of coreflection.

Русский

Согласование в обобщённой паре: конъюгация в perf-паре равна двойственному отображению соответствующей coreflection.

LaTeX

$$$ P.toPerfPair.conj (P.reflection(i)) = (P.coreflection(i)).toLinearMap.dualMap $$$

Lean4

@[simp]
theorem toPerfPair_conj_reflection : P.toPerfPair.conj (P.reflection i) = (P.coreflection i).toLinearMap.dualMap :=
  by
  ext f n
  simp [LinearEquiv.conj_apply, reflection_apply, coreflection_apply, mul_comm (f <| P.coroot i)]

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