Theorems · Definition · group theory

Units.mk.noConfusion

{α : Type u} →
  {inst : Monoid α} →
    {P : Sort u_1} →
      {val inv : α} →
        {val_inv : val * inv = 1} →
          {inv_val : inv * val = 1} →
            {val' inv' : α} →
              {val_inv' : val' * inv' = 1} →
                {inv_val' : inv' * val' = 1} →
                  { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } =
                      { val := val', inv := inv', val_inv := val_inv', inv_val := inv_val' } →
                    (val ≍ val' → inv ≍ inv' → P) → P

Defined in

Mathlib.Algebra.Group.Units.Defs

Cited by

3 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms