Theorems · Definition · number theory

LinearOrderedCommGroupWithZero.mk.noConfusion

{α : Type u_3} →
  {P : Sort u} →
    {toLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero α} →
      {toInv : Inv α} →
        {toDiv : Div α} →
          {toZPow : ZPow α} →
            {div_eq_mul_inv : autoParam (∀ (a b : α), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam} →
              {zpow_zero' : autoParam (∀ (a : α), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam} →
                {zpow_succ' :
                    autoParam (∀ (n : ℕ) (a : α), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam} →
                  {zpow_neg' :
                      autoParam (∀ (n : ℕ) (a : α), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹)
                        DivInvMonoid.zpow_neg'._autoParam} →
                    {toNontrivial : Nontrivial α} →
                      {inv_zero : 0⁻¹ = 0} →
                        {mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1} →
                          {toLinearOrderedCommMonoidWithZero' : LinearOrderedCommMonoidWithZero α} →
                            {toInv' : Inv α} →
                              {toDiv' : Div α} →
                                {toZPow' : ZPow α} →
                                  {div_eq_mul_inv' :
                                      autoParam (∀ (a b : α), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam} →
                                    {zpow_zero'' :
                                        autoParam (∀ (a : α), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam} →
                                      {zpow_succ'' :
                                          autoParam (∀ (n : ℕ) (a : α), a ^ ↑n.succ = a ^ ↑n * a)
                                            DivInvMonoid.zpow_succ'._autoParam} →
                                        {zpow_neg'' :
                                            autoParam (∀ (n : ℕ) (a : α), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹)
                                              DivInvMonoid.zpow_neg'._autoParam} →
                                          {toNontrivial' : Nontrivial α} →
                                            {inv_zero' : 0⁻¹ = 0} →
                                              {mul_inv_cancel' : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1} →
                                                {
                                                      toLinearOrderedCommMonoidWithZero :=
                                                        toLinearOrderedCommMonoidWithZero,
                                                      toInv := toInv, toDiv := toDiv, toZPow := toZPow,
                                                      div_eq_mul_inv := div_eq_mul_inv, zpow_zero' := zpow_zero',
                                                      zpow_succ' := zpow_succ', zpow_neg' := zpow_neg',
                                                      toNontrivial := toNontrivial, inv_zero := inv_zero,
                                                      mul_inv_cancel := mul_inv_cancel } =
                                                    {
                                                      toLinearOrderedCommMonoidWithZero :=
                                                        toLinearOrderedCommMonoidWithZero',
                                                      toInv := toInv', toDiv := toDiv', toZPow := toZPow',
                                                      div_eq_mul_inv := div_eq_mul_inv', zpow_zero' := zpow_zero'',
                                                      zpow_succ' := zpow_succ'', zpow_neg' := zpow_neg'',
                                                      toNontrivial := toNontrivial', inv_zero := inv_zero',
                                                      mul_inv_cancel := mul_inv_cancel' } →
                                                  (toLinearOrderedCommMonoidWithZero ≍
                                                        toLinearOrderedCommMonoidWithZero' →
                                                      toInv ≍ toInv' → toDiv ≍ toDiv' → toZPow ≍ toZPow' → P) →
                                                    P

Defined in

Mathlib.Algebra.Order.GroupWithZero.Canonical

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms