fin_two_induction — Mathlib

English

Let P be a property of SL(2,R). If P holds for all 2×2 matrices with entries a,b,c,d ∈ R satisfying ad − bc = 1, then P holds for every element of SL(2,R).

Русский

Пусть P — свойство для элементов SL(2,R). Если P выполняется для всех матриц вида \begin{pmatrix} a & b \\ c & d \end{pmatrix} с a d − b c = 1, то P выполняется для любого элемента SL(2,R).

LaTeX

$$fin_two_induction (P) (h) (g) : P g$$

Lean4

theorem fin_two_induction (P : SL(2, R) → Prop)
    (h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], by rwa [det_fin_two_of]⟩) (g : SL(2, R)) :
    P g := by
  obtain ⟨m, hm⟩ := g
  convert h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm)
  ext i j; fin_cases i <;> fin_cases j <;> rfl

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