Stream: Is there code for X?

Topic: If there is an inverse, it's unique?

Anne Baanen (Feb 26 2020 at 09:43):

What is the best way to get the result i * j = 1 → i * j' = 1 → j = j' in a comm_monoid? It seems like this would be in mathlib already but library_search doesn't find it, nor the equivalent in a general monoid.

Mario Carneiro (Feb 26 2020 at 11:30):

It exists, but the proof is buried inside units.ext.

import algebra.group.units

example {α} [comm_monoid α] (i j j' : α) :
i * j = 1 → i * j' = 1 → j = j' :=
λ h h', congr_arg units.inv \$
@units.ext _ _ (units.mk_of_mul_eq_one _ _ h) (units.mk_of_mul_eq_one _ _ h') rfl


Last updated: May 16 2021 at 05:21 UTC