Theorems · Theorem · group theory

Units.mk.injEq

∀ {α : Type u} [inst : Monoid α] (val inv : α) (val_inv : val * inv = 1) (inv_val : inv * val = 1) (val_1 inv_1 : α)
  (val_inv_1 : val_1 * inv_1 = 1) (inv_val_1 : inv_1 * val_1 = 1),
  ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } =
      { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 }) =
    (val = val_1 ∧ inv = inv_1)

Defined in

Mathlib.Algebra.Group.Units.Defs

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

Monoid