fin_two_exists_eq_mk_of_apply_zero_one_eq_zero

English

For any g ∈ SL(2,R) with g(1,0) = 0 in a field R, there exist a,b with a ≠ 0 such that g equals the matrix formed by a,b,0,a^{-1}.

Русский

Для любого g ∈ SL(2,R) с g(1,0) = 0 существует a,b с a ≠ 0, таких что g = ⟨[[a,b],[0,a^{-1}]]⟩.

LaTeX

$$∃ a,b ∈ R, ∃ h ≠ 0 : g = ⟨!![ [a, b], [0, a^{-1}] ], by simp [h]⟩$$

Lean4

theorem fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type*} [Field R] (g : SL(2, R)) (hg : g 1 0 = 0) :
    ∃ (a b : R) (h : a ≠ 0), g = (⟨!![a, b; 0, a⁻¹], by simp [h]⟩ : SL(2, R)) := by
  induction g using Matrix.SpecialLinearGroup.fin_two_induction with
  | h a b c d h_det =>
    replace hg : c = 0 := by simpa using hg
    have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det
    refine ⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩
    simp_rw [eq_inv_of_mul_eq_one_right had, hg]

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