of_mem_specialOrthogonalGroup_fin_two_iff

English

For 2×2 matrices, a matrix belongs to the special orthogonal group iff it satisfies explicit relations a=d, b=-c, and a^2+b^2=1.

Русский

Для 2×2 матриц принадлежность к специальной ортогональной группе эквивалентна выполнению явных условий a=d, b=-c и a^2+b^2=1.

LaTeX

$$$M = \\begin{pmatrix} a & b \\\\ c & d \\end{pmatrix} \\in \\mathrm{specialOrthogonalGroup}(\\mathrm{Fin}(2),R) \\iff a=d \\land b=-c \\land a^2+b^2=1$$$

Lean4

@[simp]
theorem of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
    !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1 :=
  by
  trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
  ·
    simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff, Fin.forall_fin_succ,
      Matrix.vecHead, Matrix.vecTail]
  refine ⟨?_, ?_⟩
  · rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
    refine ⟨?_, ?_, ?_⟩
    · linear_combination -a * h₂ + c * h₁ + d * h₃
    · linear_combination -c * h₀ + a * h₁ - b * h₃
    · linear_combination h₀
  · rintro ⟨rfl, rfl, H⟩
    ring_nf at H ⊢
    tauto

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