pso_inv — Mathlib

English

There is a constructive inverse for Pso, given i^2 = -1.

Русский

Существует конструктивно заданная обратная для Pso при i^2 = -1.

LaTeX

$$$$ \text{invertible}(Pso(p,q,R,i)) \text{ exists, given } i^2 = -1. $$$$

Lean4

theorem pso_inv {i : R} (hi : i * i = -1) : Pso p q R i * Pso p q R (-i) = 1 :=
  by
  ext (x y); rcases x with ⟨x⟩ | ⟨x⟩ <;> rcases y with ⟨y⟩ | ⟨y⟩
  · -- x y : p
    by_cases h : x = y <;> simp [Pso, h, one_apply]
  · -- x : p, y : q
    simp [Pso]
  · -- x : q, y : p
    simp [Pso]
  · -- x y : q
    by_cases h : x = y <;> simp [Pso, h, hi, one_apply]

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