Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c
Demostrar con Lean4 que si \(G\) es un grupo y \(a, b, c ∈ G\) tales que \(a·b = a·c\), entonces \(b = c\).
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b c : G} example (h: a * b = a * c) : b = c := sorry |
Read More «Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c»