def f {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (g : G) : X → X

Defs used throughout.

Equations

• f g x = g • x

theorem fcomp {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (g h : G) : (fun (x : X) => (g * h) • x) = (fun (x : X) => g • x) ∘ fun (x : X) => h • x

theorem finj {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (g : G) : Function.Injective fun (x : X) => g • x

@[reducible, inline]

abbrev FG2 : Type

Equations

• FG2 = FreeGroup (Fin 2)

def σchar : Fin 2

Equations

• σchar = 0

def τchar : Fin 2

Equations

• τchar = 1

theorem σ_def : σchar = 0

theorem τ_def : τchar = 1

@[reducible, inline]

abbrev σ : FreeGroup (Fin 2)

Equations

• σ = FreeGroup.of σchar

@[reducible, inline]

abbrev τ : FreeGroup (Fin 2)

Equations

• τ = FreeGroup.of τchar

@[reducible, inline]

abbrev chartype : Type

Equations

• chartype = (Fin 2 × Bool)

instance finite_chartype : Finite chartype

instance countable_chartype : Countable chartype

instance countable_of_fg2 : Countable FG2

theorem wopts (w : chartype) : w = (0, true) ∨ w = (0, false) ∨ w = (1, true) ∨ w = (1, false)

theorem split2 (i : Fin 2) : i = 0 ∨ i = 1

@[reducible, inline]

abbrev MAT : Type

Equations

• MAT = Matrix (Fin 3) (Fin 3) ℝ

@[reducible, inline]

abbrev R3_raw : Type

Equations

• R3_raw = (Fin 3 → ℝ)

@[reducible, inline]

abbrev R3 : Type

Equations

• R3 = EuclideanSpace ℝ (Fin 3)

def to_R3 (v : R3_raw) : R3

Equations

• to_R3 v = WithLp.toLp 2 v

def origin : R3

Equations

• origin = 0

def S2 : Set R3

Equations

• S2 = Metric.sphere 0 1

@[reducible, inline]

abbrev SO3 : Submonoid (Matrix (Fin 3) (Fin 3) ℝ)

Equations

• SO3 = Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem so3_invs_coe (g : ↥SO3) : (↑g)⁻¹ = ↑g⁻¹

theorem unitary_invs_coe (g : ↥(Matrix.orthogonalGroup (Fin 3) ℝ)) : (↑g)⁻¹ = ↑g⁻¹

instance so3_has_inv (g : ↥SO3) : Invertible ↑g

Equations

• so3_has_inv g = (↑g).invertibleOfRightInverse (↑g).transpose ⋯

theorem so3_closed_under_inverse (g : MAT) : g ∈ SO3 → g⁻¹ ∈ SO3

instance SO3_action_on_MAT : MulAction (↥SO3) R3_raw

Equations

• SO3_action_on_MAT = { smul := fun (g : ↥SO3) (v : R3_raw) => (↑g).mulVec v, mul_smul := SO3_action_on_MAT._proof_1, one_smul := SO3_action_on_MAT._proof_2 }

instance SO3_action_on_R3 : MulAction (↥SO3) R3

Equations

• SO3_action_on_R3 = inferInstance

theorem SO3_smul_def (g : ↥SO3) (v : R3) : g • v = to_R3 ((↑g).mulVec v.ofLp)

noncomputable def normed : R3 → R3

Equations

• normed x = (1 / ‖x‖) • x

theorem normed_in_S2 {v : R3} : v ≠ 0 → normed v ∈ S2

theorem ml {i j : ℕ} {m n : Fin (i * j)} : m ≠ n → m.divNat ≠ n.divNat ∨ m.divNat = n.divNat ∧ m.modNat ≠ n.modNat

theorem ml2 {i j : ℕ} {m n : Fin (i * j)} : m ≠ n → m.modNat ≠ n.modNat ∨ m.modNat = n.modNat ∧ m.divNat ≠ n.divNat