Created
October 23, 2025 05:35
-
-
Save Iainmon/128289a1b37452d670982d7b89fb0aaa to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Init.Core | |
| import Init.Prelude | |
| import Mathlib.Algebra.Group.Defs | |
| import Mathlib.Tactic | |
| namespace Q10 | |
| class Req (α : Type) extends Semigroup α where | |
| eᵣ : α | |
| unit_right : ∀ a : α, a * eᵣ = a | |
| invᵣ : α → α | |
| invᵣ_spec : ∀ a : α, a * invᵣ a = eᵣ | |
| attribute [simp] Req.unit_right Req.invᵣ_spec | |
| instance Req.One {α : Type} [r : Req α] : One α where | |
| one := r.eᵣ | |
| instance Req.Mul {α : Type} [r : Req α] : Mul α where | |
| mul a b := a * b | |
| instance Req.Inv {α : Type} [r : Req α] : Inv α where | |
| inv a := r.invᵣ a | |
| @[simp] | |
| lemma Req.mul_one [Req α] : ∀ (a : α), a * (1 : α) = a := by intro a ; simp only [OfNat.ofNat,One.one,unit_right] | |
| @[simp] | |
| lemma Req.mul_inv_cancel [Req α] : ∀ (a : α), a * a⁻¹ = (1 : α) := by intro a ; simp only [Inv.inv, Req.invᵣ_spec, OfNat.ofNat, One.one] | |
| -- @[simp] | |
| -- lemma Req.inv_one [r : Req α] : (1 : α)⁻¹ = (1 : α) := by | |
| -- @[simp] | |
| -- lemma Req.inv_inv [Req α] : ∀ (a : α), (a⁻¹)⁻¹ = a := by | |
| @[simp] | |
| lemma Req.mul_right_cancel {α : Type} [r : Req α] : ∀ (x y a : α), x * a = y * a -> x = y := by | |
| intros x y a h₁ | |
| have h₂ : x * a * a⁻¹ = y * a * a⁻¹ := by simp_all only [mul_assoc,mul_inv_cancel,mul_one] | |
| simp only [mul_assoc, mul_inv_cancel, mul_one] at h₂ ; simp_all only [] | |
| instance Req.IsRightCancelMul [r : Req α] : IsRightCancelMul α where | |
| mul_right_cancel x a y h := by exact Req.mul_right_cancel x y a h | |
| instance [Req α] : Semigroup α := by (expose_names; exact inst.toSemigroup) | |
| @[simp] | |
| lemma Req.inv_is_left [r : Req α] : ∀ (a : α), a⁻¹ * a = (1 : α) := by | |
| intros a ; let b := a⁻¹ ; let c := b⁻¹ | |
| have hb : a * b = (1 : α) := by exact Req.mul_inv_cancel a | |
| have hc : b * c = (1 : α) := by exact Req.mul_inv_cancel (a⁻¹) | |
| have h1 : a * (1 : α) = (1 : α) * c := by | |
| calc | |
| a * (1 : α) = a * (b * c) := by rw [hc] | |
| _ = (a * b) * c := by simp only [mul_assoc] | |
| _ = (1 : α) * c := by rw [hb] | |
| calc | |
| b * a = b * ((1 : α) * c) := by rw [<-h1,Req.mul_one] | |
| _ = (b * (1 : α)) * c := by rw [mul_assoc] | |
| _ = b * c := by simp only [OfNat.ofNat, One.one, unit_right] | |
| _ = (1 : α) := by exact hc | |
| @[simp] | |
| lemma Req.left_unit {α : Type} [r : Req α] : ∀ (a : α), (1 : α) * a = a := by | |
| intros a | |
| rw [<-Req.mul_inv_cancel,mul_assoc,Req.inv_is_left,Req.mul_one] | |
| instance Req.Monoid {α : Type} [Req α] : Monoid α where | |
| one_mul a := Req.left_unit a | |
| mul_one a := Req.mul_one a | |
| instance Req.Group {α : Type} [Req α] : Group α where | |
| inv_mul_cancel a := by exact (Req.inv_is_left a) | |
| end Q10 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment