pointReflection_fixed_iff_of_module

English

In the module setting with invertible 2, the fixed point condition is equivalent to y = x.

Русский

В условиях модуля и инвертируемости 2 фиксированная точка эквивалентна y = x.

LaTeX

$$pointReflection_fixed_iff_of_module [Invertible(2:k)] {x y} : pointReflection k x y = y ↔ y = x$$

Lean4

theorem pointReflection_fixed_iff_of_module [Invertible (2 : k)] {x y : P₁} : pointReflection k x y = y ↔ y = x :=
  ((injective_pointReflection_left_of_module k y).eq_iff' (pointReflection_self k y)).trans eq_comm

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