English
If a set G has a binary operation that is associative, has a left identity, and each element has a left inverse, then G can be equipped with a group structure.
Русский
Если множество G с бинарной операцией ассоциативно, имеет левый нейтральный элемент и у каждого элемента есть левый обратный, то на G можно возвести группу.
LaTeX
$$$\\\\exists G, \\\\[Mul G] \\\\[Inv G] \\\\[One G] \\\\Rightarrow (\\\\forall a,b,c \\\\\\in G, (a*b)*c = a*(b*c)) \\\\land (\\\\forall a, 1*a = a) \\\\land (\\\\forall a, a^{-1}*a = 1) \\\\Rightarrow Group G$$$
Lean4
/-- Define a `Group` structure on a Type by proving `∀ a, a * 1 = a` and
`∀ a, a * a⁻¹ = 1`.
Note that this uses the default definitions for `npow`, `zpow` and `div`.
See note [reducible non-instances]. -/
@[to_additive /-- Define an `AddGroup` structure on a Type by proving `∀ a, a + 0 = a` and
`∀ a, a + -a = 0`.
Note that this uses the default definitions for `nsmul`, `zsmul` and `sub`.
See note [reducible non-instances]. -/
]
abbrev ofRightAxioms {G : Type u} [Mul G] [Inv G] [One G] (assoc : ∀ a b c : G, (a * b) * c = a * (b * c))
(mul_one : ∀ a : G, a * 1 = a) (mul_inv_cancel : ∀ a : G, a * a⁻¹ = 1) : Group G :=
have inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1 := fun a =>
calc
a⁻¹ * a = (a⁻¹ * a) * 1 := (mul_one _).symm
_ = (a⁻¹ * a) * ((a⁻¹ * a) * (a⁻¹ * a)⁻¹) := by rw [mul_inv_cancel]
_ = ((a⁻¹ * (a * a⁻¹)) * a) * (a⁻¹ * a)⁻¹ := by simp only [assoc]
_ = 1 := by rw [mul_inv_cancel, mul_one, mul_inv_cancel]
{ mul_assoc := assoc, mul_one := mul_one, inv_mul_cancel := inv_mul_cancel,
one_mul := fun a => by rw [← mul_inv_cancel a, assoc, inv_mul_cancel, mul_one] }
