noncomputable def sq_2 : ℝ

Equations

• sq_2 = Real.sqrt 2

theorem pi_sqrt_two (h : ∃ (x : ℚ), Real.pi = ↑x * sq_2) : false = true

theorem sin_sqrt_2_neq_0 : Real.sin sq_2 = 0 → false = true

noncomputable def rot_sq_2 : Matrix (Fin 3) (Fin 3) ℝ

Equations

• rot_sq_2 = Matrix.of ![![Real.cos sq_2, -Real.sin sq_2, 0], ![Real.sin sq_2, Real.cos sq_2, 0], ![0, 0, 1]]

theorem rot_sq_2_det_ne_zero : Matrix.det rot_sq_2 ≠ 0

noncomputable def gl_sq_2 : GL (Fin 3) ℝ

Equations

• gl_sq_2 = Matrix.GeneralLinearGroup.mkOfDetNeZero rot_sq_2 rot_sq_2_det_ne_zero

theorem coe_gl_sq_2_eq_rot_sq_2 : ↑gl_sq_2 = rot_sq_2

noncomputable def rot_sq_2_inv : Matrix (Fin 3) (Fin 3) ℝ

Equations

• rot_sq_2_inv = Matrix.of ![![Real.cos sq_2, Real.sin sq_2, 0], ![-Real.sin sq_2, Real.cos sq_2, 0], ![0, 0, 1]]

theorem det_sq_2_inv_ne_zero : Matrix.det rot_sq_2_inv ≠ 0

noncomputable def gl_sq_2_inv : GL (Fin 3) ℝ

Equations

• gl_sq_2_inv = Matrix.GeneralLinearGroup.mkOfDetNeZero rot_sq_2_inv det_sq_2_inv_ne_zero

theorem coe_gl_sq_2_inv_eq_rot_sq_2_inv : ↑gl_sq_2_inv = rot_sq_2_inv