Theorems · Theorem · group theory

Units.mk.inj

∀ {α : 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

2 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms