@[reducible, inline]

abbrev DehnInvariant.tensorProduct (G : Type u) (H : Type v) [AddCommGroup G] [AddCommGroup H] : Type (max u v)

def DehnInvariant.tmul {G : Type u} {H : Type v} [AddCommGroup G] [AddCommGroup H] (g : G) (h : H) : tensorProduct G H

theorem DehnInvariant.tensorProduct_proposition {G : Type u} {H : Type v} [AddCommGroup G] [AddCommGroup H] : (∀ (g : G) (h : H), tmul 0 h = 0 ∧ tmul g 0 = 0) ∧ (∀ (a : ℤ) (g : G) (h : H), tmul (a • g) h = a • tmul g h ∧ tmul g (a • h) = a • tmul g h) ∧ ∀ (s : Set G) (t : Set H), Submodule.span ℤ s = ⊤ → Submodule.span ℤ t = ⊤ → Submodule.span ℤ (Set.image2 (fun (g : G) (h : H) => tmul g h) s t) = ⊤

theorem DehnInvariant.arccos_one_third_div_pi_irrational : Irrational (Real.arccos (1 / 3) / Real.pi)

@[reducible, inline]

abbrev DehnInvariant.DehnGroup : Type

structure DehnInvariant.Edge : Type

• length : ℝ
• angle : ℝ

noncomputable def DehnInvariant.dehnInvariant (edges : List Edge) : DehnGroup

noncomputable def DehnInvariant.tetrahedralAngle : ℝ

noncomputable def DehnInvariant.fBar (f : ℝ →ₗ[ℚ] ℝ) (hf_pi : f Real.pi = 0) : AddCircle (2 * Real.pi) →+ ℝ

@[simp]

theorem DehnInvariant.fBar_mk (f : ℝ →ₗ[ℚ] ℝ) (hf_pi : f Real.pi = 0) (x : ℝ) : (fBar f hf_pi) ↑x = f x

theorem DehnInvariant.exists_linearMap_of_irrational {α : ℝ} (hirr : Irrational (α / Real.pi)) : ∃ (f : ℝ →ₗ[ℚ] ℝ), f Real.pi = 0 ∧ f α ≠ 0

theorem DehnInvariant.tmul_ne_zero_of_irrational {α ℓ : ℝ} (hℓ : ℓ ≠ 0) (hirr : Irrational (α / Real.pi)) : ℓ ⊗ₜ[ℤ] ↑α ≠ 0

theorem DehnInvariant.dehn_cube (ℓ : ℝ) : (12 • ℓ) ⊗ₜ[ℤ] ↑(Real.pi / 2) = 0

theorem DehnInvariant.dehn_tetrahedron_ne_zero {ℓ : ℝ} (hℓ : ℓ ≠ 0) : (6 • ℓ) ⊗ₜ[ℤ] ↑tetrahedralAngle ≠ 0

theorem DehnInvariant.dehn_cube_ne_dehn_tetrahedron {ℓ ℓ' : ℝ} (hℓ' : ℓ' ≠ 0) : (12 • ℓ) ⊗ₜ[ℤ] ↑(Real.pi / 2) ≠ (6 • ℓ') ⊗ₜ[ℤ] ↑tetrahedralAngle