coreflection_eq_flip_reflection — Mathlib

English

Let P be a RootPairing on index set ι with a commutative ring R and M, N as modules. Then for every i ∈ ι, the coreflection at i equals the flip-reflection at i: coreflection_i = flip.reflection_i.

Русский

Пусть P — RootPairing на множество индексов ι над кольцом R и модулями M, N. Тогда для каждого i ∈ ι корефлексия в точке i равна отражению, полученному от операции flip: coreflection_i = flip.reflection_i.

LaTeX

$$$\forall i \in \iota:\; P.coreflection(i) = P.flip.reflection(i)$$$

Lean4

theorem coreflection_eq_flip_reflection : P.coreflection i = P.flip.reflection i :=
  rfl

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