theorem coe_gl_one_eq_one : gl_one = 1

theorem coe_gl_a_eq_matrix_a : ↑gl_a = matrix_a

theorem coe_gl_a_inv_eq_matrix_a_inv : ↑gl_a' = matrix_a'

theorem coe_gl_b_eq_matrix_b : ↑gl_b = matrix_b

theorem coe_gl_b_inv_eq_matrix_b_inv : ↑gl_b' = matrix_b'

noncomputable def a_b_c_vec (a : ℤ) (b : ℤ) (c : ℤ) (n : ℕ) : r_3

Equations

• a_b_c_vec a b c n = ![1 / 3 ^ n * ↑a * Real.sqrt 2, 1 / 3 ^ n * ↑b, 1 / 3 ^ n * ↑c * Real.sqrt 2]

theorem rotate_mul (p1 : GL (Fin 3) ℝ) (p2 : GL (Fin 3) ℝ) (i : r_3) : rotate (p1 * p2) i = rotate p2 (rotate p1 i)

theorem rotate_preserve_gl_a (n1 : ℕ) (a1 : ℤ) (b1 : ℤ) (c1 : ℤ) (i : r_3) (h : i = a_b_c_vec a1 b1 c1 n1) : rotate gl_a i = a_b_c_vec (3 * a1) (b1 + 4 * c1) (-2 * b1 + c1) (n1 + 1)

theorem rotate_preserve_gl_a' (n1 : ℕ) (a1 : ℤ) (b1 : ℤ) (c1 : ℤ) (i : r_3) (h : i = a_b_c_vec a1 b1 c1 n1) : rotate gl_a' i = a_b_c_vec (3 * a1) (b1 - 4 * c1) (2 * b1 + c1) (n1 + 1)

theorem rotate_preserve_gl_b (n1 : ℕ) (a1 : ℤ) (b1 : ℤ) (c1 : ℤ) (i : r_3) (h : i = a_b_c_vec a1 b1 c1 n1) : rotate gl_b i = a_b_c_vec (a1 + 2 * b1) (-4 * a1 + b1) (3 * c1) (n1 + 1)

theorem rotate_preserve_gl_b' (n1 : ℕ) (a1 : ℤ) (b1 : ℤ) (c1 : ℤ) (i : r_3) (h : i = a_b_c_vec a1 b1 c1 n1) : rotate gl_b' i = a_b_c_vec (a1 - 2 * b1) (4 * a1 + b1) (3 * c1) (n1 + 1)

theorem lemma_3_1 {n : ℕ} (p : List (erzeuger_t × Bool)) (h : List.length p = n) : ∃ (a : ℤ) (b : ℤ) (c : ℤ), rotate (list_to_matrix p) zero_one_zero = a_b_c_vec a b c n