def matrix_a : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_a = !![1, 0, 0; 0, 1 / 3, -2 / 3 * √2; 0, 2 / 3 * √2, 1 / 3]

def matrix_a' : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_a' = !![1, 0, 0; 0, 1 / 3, 2 / 3 * √2; 0, -2 / 3 * √2, 1 / 3]

def matrix_b : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_b = !![1 / 3, -2 / 3 * √2, 0; 2 / 3 * √2, 1 / 3, 0; 0, 0, 1]

def matrix_b' : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_b' = !![1 / 3, 2 / 3 * √2, 0; -2 / 3 * √2, 1 / 3, 0; 0, 0, 1]

def matrix_one : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_one = 1

theorem matrix_a_det_neq_zero : matrix_a.det ≠ 0

theorem matrix_a'_det_neq_zero : matrix_a'.det ≠ 0

theorem matrix_b_det_neq_zero : matrix_b.det ≠ 0

theorem matrix_b'_det_neq_zero : matrix_b'.det ≠ 0

theorem matrix_one_det_neq_zero : matrix_one.det ≠ 0

def gl_a : GL (Fin 3) ℝ

Equations

• gl_a = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_a matrix_a_det_neq_zero

def gl_a' : GL (Fin 3) ℝ

Equations

• gl_a' = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_a' matrix_a'_det_neq_zero

def gl_b : GL (Fin 3) ℝ

Equations

• gl_b = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_b matrix_b_det_neq_zero

def gl_b' : GL (Fin 3) ℝ

Equations

• gl_b' = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_b' matrix_b'_det_neq_zero

def gl_one : GL (Fin 3) ℝ

Equations

• gl_one = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_one matrix_one_det_neq_zero

def generator : Set (GL (Fin 3) ℝ)

Equations

• generator = {gl_a, gl_b}

def G : Subgroup (GL (Fin 3) ℝ)

Equations

• G = Subgroup.closure generator

@[reducible, inline]

abbrev r_3 : Type

Equations

• r_3 = (Fin 3 → ℝ)

@[reducible, inline]

abbrev r_2 : Type

Equations

• r_2 = (Fin 2 → ℝ)

def zero_one_zero : r_3

Equations

• zero_one_zero = ![0, 1, 0]

def rotate (p : GL (Fin 3) ℝ) (vec : r_3) : r_3

Equations

• rotate p vec = Matrix.vecMul vec ↑p

def rotate_set (x : Set r_3) (p : GL (Fin 3) ℝ) : Set r_3

Equations

• rotate_set x p = {w : r_3 | ∃ v ∈ x, rotate p v = w}

def rotate_n_times (n : ℕ) (p : GL (Fin 3) ℝ) (vec : r_3) : r_3

Equations

• rotate_n_times 0 p vec = vec
• rotate_n_times m.succ p vec = rotate_n_times m p (rotate p vec)

def translate (p vec : r_3) : r_3

Equations

• translate p vec = p + vec

def unitBall : Set (Fin 3 → ℝ)

Equations

• unitBall = Euclidean.closedBall ![0, 0, 0] 1

def origin : r_3

Equations

• origin = ![0, 0, 0]

def unitBall_without_origin : Set (Fin 3 → ℝ)

Equations

• unitBall_without_origin = unitBall \ {origin}

def fixpoint (y : r_3) (p : GL (Fin 3) ℝ) : Prop

Equations

• fixpoint y p = (rotate p y = y)

def D : Set ↑unitBall_without_origin

Equations

• D = {w : ↑unitBall_without_origin | ∀ (p : ↥G), fixpoint ↑w ↑p}

def RotationAxis (p : GL (Fin 3) ℝ) : Set r_3

Equations

• RotationAxis p = {w : r_3 | fixpoint w p}