Theorems · Definition · number theory

LinearOrderedCommGroupWithZero.recOn

{α : Type u_3} →
  {motive : LinearOrderedCommGroupWithZero α → Sort u} →
    (t : LinearOrderedCommGroupWithZero α) →
      ([toLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero α] →
          [toInv : Inv α] →
            [toDiv : Div α] →
              [toZPow : ZPow α] →
                (div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹) →
                  (zpow_zero' : ∀ (a : α), a ^ 0 = 1) →
                    (zpow_succ' : ∀ (n : ℕ) (a : α), a ^ ↑n.succ = a ^ ↑n * a) →
                      (zpow_neg' : ∀ (n : ℕ) (a : α), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) →
                        [toNontrivial : Nontrivial α] →
                          (inv_zero : 0⁻¹ = 0) →
                            (mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1) →
                              motive
                                { 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 }) →
        motive t

Defined in

Mathlib.Algebra.Order.GroupWithZero.Canonical

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms