Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

24191 views
License: APACHE
-- Typing `rw mul_inv` and then looking at possible completions
-- gives you `mul_inv_rev`, which is the way to start this off.

example (G : Type) [group G] (g h k : G) : (g * h * k⁻¹)⁻¹ = k * h⁻¹ * g⁻¹ :=
begin
  rw mul_inv_rev,
  rw inv_inv,
  rw mul_inv_rev,
  rw mul_assoc,
end

example (G : Type) [group G] (g h k : G) : (g * h * k⁻¹)⁻¹ = k * h⁻¹ * g⁻¹ :=
begin
  rw [mul_inv_rev, inv_inv, mul_inv_rev, mul_assoc]
end

example (G : Type) [group G] (g h k : G) : (g * h * k⁻¹)⁻¹ = k * h⁻¹ * g⁻¹ :=
begin
 simp [mul_assoc],
end