rightAngleRotation_trans_neg_orientation

English

For the negated orientation, the associated rotation equals the original rotation composed with negation: (-o).rightAngleRotation = o.rightAngleRotation.trans (neg).

Русский

Для отрицательной ориентации: (-o).rightAngleRotation = o.rightAngleRotation.trans (neg).

LaTeX

$$$(-o).rightAngleRotation = o.rightAngleRotation.trans (\\\\mathrm{neg})$$$

Lean4

@[simp]
theorem rightAngleRotation_trans_neg_orientation :
    (-o).rightAngleRotation = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ) :=
  LinearIsometryEquiv.ext <| o.rightAngleRotation_neg_orientation

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