Theorems · Definition · group theory

CommGroupWithZero.recOn

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

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms