Theorems · Definition · field theory

Field.mk.noConfusion

{K : Type u} →
  {P : Sort u_1} →
    {toCommRing : CommRing K} →
      {toInv : Inv K} →
        {toDiv : Div K} →
          {toZPow : ZPow K} →
            {div_eq_mul_inv : autoParam (∀ (a b : K), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam} →
              {zpow_zero' : autoParam (∀ (a : K), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam} →
                {zpow_succ' :
                    autoParam (∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam} →
                  {zpow_neg' :
                      autoParam (∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹)
                        DivInvMonoid.zpow_neg'._autoParam} →
                    {toNontrivial : Nontrivial K} →
                      {toNNRatCast : NNRatCast K} →
                        {toRatCast : RatCast K} →
                          {mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1} →
                            {inv_zero : 0⁻¹ = 0} →
                              {nnratCast_def :
                                  autoParam (∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) DivisionRing.nnratCast_def._autoParam} →
                                {nnqsmul : ℚ≥0 → K → K} →
                                  {nnqsmul_def :
                                      autoParam (∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a)
                                        DivisionRing.nnqsmul_def._autoParam} →
                                    {ratCast_def :
                                        autoParam (∀ (q : ℚ), ↑q = ↑q.num / ↑q.den)
                                          DivisionRing.ratCast_def._autoParam} →
                                      {qsmul : ℚ → K → K} →
                                        {qsmul_def :
                                            autoParam (∀ (a : ℚ) (x : K), qsmul a x = ↑a * x)
                                              DivisionRing.qsmul_def._autoParam} →
                                          {toCommRing' : CommRing K} →
                                            {toInv' : Inv K} →
                                              {toDiv' : Div K} →
                                                {toZPow' : ZPow K} →
                                                  {div_eq_mul_inv' :
                                                      autoParam (∀ (a b : K), a / b = a * b⁻¹)
                                                        DivInvMonoid.div_eq_mul_inv._autoParam} →
                                                    {zpow_zero'' :
                                                        autoParam (∀ (a : K), a ^ 0 = 1)
                                                          DivInvMonoid.zpow_zero'._autoParam} →
                                                      {zpow_succ'' :
                                                          autoParam (∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a)
                                                            DivInvMonoid.zpow_succ'._autoParam} →
                                                        {zpow_neg'' :
                                                            autoParam
                                                              (∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹)
                                                              DivInvMonoid.zpow_neg'._autoParam} →
                                                          {toNontrivial' : Nontrivial K} →
                                                            {toNNRatCast' : NNRatCast K} →
                                                              {toRatCast' : RatCast K} →
                                                                {mul_inv_cancel' : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1} →
                                                                  {inv_zero' : 0⁻¹ = 0} →
                                                                    {nnratCast_def' :
                                                                        autoParam (∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den)
                                                                          DivisionRing.nnratCast_def._autoParam} →
                                                                      {nnqsmul' : ℚ≥0 → K → K} →
                                                                        {nnqsmul_def' :
                                                                            autoParam
                                                                              (∀ (q : ℚ≥0) (a : K),
                                                                                nnqsmul' q a = ↑q * a)
                                                                              DivisionRing.nnqsmul_def._autoParam} →
                                                                          {ratCast_def' :
                                                                              autoParam
                                                                                (∀ (q : ℚ), ↑q = ↑q.num / ↑q.den)
                                                                                DivisionRing.ratCast_def._autoParam} →
                                                                            {qsmul' : ℚ → K → K} →
                                                                              {qsmul_def' :
                                                                                  autoParam
                                                                                    (∀ (a : ℚ) (x : K),
                                                                                      qsmul' a x = ↑a * x)
                                                                                    DivisionRing.qsmul_def._autoParam} →
                                                                                { toCommRing := toCommRing,
                                                                                      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,
                                                                                      toNNRatCast := toNNRatCast,
                                                                                      toRatCast := toRatCast,
                                                                                      mul_inv_cancel := mul_inv_cancel,
                                                                                      inv_zero := inv_zero,
                                                                                      nnratCast_def := nnratCast_def,
                                                                                      nnqsmul := nnqsmul,
                                                                                      nnqsmul_def := nnqsmul_def,
                                                                                      ratCast_def := ratCast_def,
                                                                                      qsmul := qsmul,
                                                                                      qsmul_def := qsmul_def } =
                                                                                    { toCommRing := toCommRing',
                                                                                      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',
                                                                                      toNNRatCast := toNNRatCast',
                                                                                      toRatCast := toRatCast',
                                                                                      mul_inv_cancel := mul_inv_cancel',
                                                                                      inv_zero := inv_zero',
                                                                                      nnratCast_def := nnratCast_def',
                                                                                      nnqsmul := nnqsmul',
                                                                                      nnqsmul_def := nnqsmul_def',
                                                                                      ratCast_def := ratCast_def',
                                                                                      qsmul := qsmul',
                                                                                      qsmul_def := qsmul_def' } →
                                                                                  (toCommRing ≍ toCommRing' →
                                                                                      toInv ≍ toInv' →
                                                                                        toDiv ≍ toDiv' →
                                                                                          toZPow ≍ toZPow' →
                                                                                            toNNRatCast ≍ toNNRatCast' →
                                                                                              toRatCast ≍ toRatCast' →
                                                                                                nnqsmul ≍ nnqsmul' →
                                                                                                  qsmul ≍ qsmul' → P) →
                                                                                    P

Defined in

Mathlib.Algebra.Field.Defs

Cited by

0 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Quot.sound