Documentation

Mathlib.Algebra.Group.Basic

Basic lemmas about semigroups, monoids, and groups #

This file lists various basic lemmas about semigroups, monoids, and groups. Most proofs are one-liners from the corresponding axioms. For the definitions of semigroups, monoids and groups, see Algebra/Group/Defs.lean.

@[simp]
theorem dite_smul {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a : α) (b : pβ) (c : ¬pβ) :
(if h : p then b h else c h) a = if h : p then b h a else c h a
@[simp]
theorem pow_dite {α : Type u_1} {β : Type u_2} [Pow α β] (p : Prop) [Decidable p] (a : α) (b : pβ) (c : ¬pβ) :
(a ^ if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h
@[simp]
theorem smul_dite {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a : pα) (b : ¬pα) (c : β) :
(c if h : p then a h else b h) = if h : p then c a h else c b h
@[simp]
theorem dite_pow {α : Type u_1} {β : Type u_2} [Pow α β] (p : Prop) [Decidable p] (a : pα) (b : ¬pα) (c : β) :
(if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c
@[simp]
theorem ite_smul {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a : α) (b : β) (c : β) :
(if p then b else c) a = if p then b a else c a
@[simp]
theorem pow_ite {α : Type u_1} {β : Type u_2} [Pow α β] (p : Prop) [Decidable p] (a : α) (b : β) (c : β) :
(a ^ if p then b else c) = if p then a ^ b else a ^ c
@[simp]
theorem smul_ite {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a : α) (b : α) (c : β) :
(c if p then a else b) = if p then c a else c b
@[simp]
theorem ite_pow {α : Type u_1} {β : Type u_2} [Pow α β] (p : Prop) [Decidable p] (a : α) (b : α) (c : β) :
(if p then a else b) ^ c = if p then a ^ c else b ^ c
@[simp]
theorem ite_vadd {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a : α) (b : β) (c : β) :
(if p then b else c) +ᵥ a = if p then b +ᵥ a else c +ᵥ a
@[simp]
theorem dite_vadd {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a : α) (b : pβ) (c : ¬pβ) :
(if h : p then b h else c h) +ᵥ a = if h : p then b h +ᵥ a else c h +ᵥ a
@[simp]
theorem vadd_dite {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a : pα) (b : ¬pα) (c : β) :
(c +ᵥ if h : p then a h else b h) = if h : p then c +ᵥ a h else c +ᵥ b h
@[simp]
theorem vadd_ite {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a : α) (b : α) (c : β) :
(c +ᵥ if p then a else b) = if p then c +ᵥ a else c +ᵥ b
theorem add_right_injective {G : Type u_3} [Add G] [IsLeftCancelAdd G] (a : G) :
Function.Injective fun (x : G) => a + x
theorem mul_right_injective {G : Type u_3} [Mul G] [IsLeftCancelMul G] (a : G) :
Function.Injective fun (x : G) => a * x
@[simp]
theorem add_right_inj {G : Type u_3} [Add G] [IsLeftCancelAdd G] (a : G) {b : G} {c : G} :
a + b = a + c b = c
@[simp]
theorem mul_right_inj {G : Type u_3} [Mul G] [IsLeftCancelMul G] (a : G) {b : G} {c : G} :
a * b = a * c b = c
theorem add_ne_add_right {G : Type u_3} [Add G] [IsLeftCancelAdd G] (a : G) {b : G} {c : G} :
a + b a + c b c
theorem mul_ne_mul_right {G : Type u_3} [Mul G] [IsLeftCancelMul G] (a : G) {b : G} {c : G} :
a * b a * c b c
theorem add_left_injective {G : Type u_3} [Add G] [IsRightCancelAdd G] (a : G) :
Function.Injective fun (x : G) => x + a
theorem mul_left_injective {G : Type u_3} [Mul G] [IsRightCancelMul G] (a : G) :
Function.Injective fun (x : G) => x * a
@[simp]
theorem add_left_inj {G : Type u_3} [Add G] [IsRightCancelAdd G] (a : G) {b : G} {c : G} :
b + a = c + a b = c
@[simp]
theorem mul_left_inj {G : Type u_3} [Mul G] [IsRightCancelMul G] (a : G) {b : G} {c : G} :
b * a = c * a b = c
theorem add_ne_add_left {G : Type u_3} [Add G] [IsRightCancelAdd G] (a : G) {b : G} {c : G} :
b + a c + a b c
theorem mul_ne_mul_left {G : Type u_3} [Mul G] [IsRightCancelMul G] (a : G) {b : G} {c : G} :
b * a c * a b c
instance AddSemigroup.to_isAssociative {α : Type u_1} [AddSemigroup α] :
Std.Associative fun (x x_1 : α) => x + x_1
Equations
  • =
instance Semigroup.to_isAssociative {α : Type u_1} [Semigroup α] :
Std.Associative fun (x x_1 : α) => x * x_1
Equations
  • =
@[simp]
theorem comp_add_left {α : Type u_1} [AddSemigroup α] (x : α) (y : α) :
((fun (x_1 : α) => x + x_1) fun (x : α) => y + x) = fun (x_1 : α) => x + y + x_1

Composing two additions on the left by y then x is equal to an addition on the left by x + y.

@[simp]
theorem comp_mul_left {α : Type u_1} [Semigroup α] (x : α) (y : α) :
((fun (x_1 : α) => x * x_1) fun (x : α) => y * x) = fun (x_1 : α) => x * y * x_1

Composing two multiplications on the left by y then x is equal to a multiplication on the left by x * y.

@[simp]
theorem comp_add_right {α : Type u_1} [AddSemigroup α] (x : α) (y : α) :
((fun (x_1 : α) => x_1 + x) fun (x : α) => x + y) = fun (x_1 : α) => x_1 + (y + x)

Composing two additions on the right by y and x is equal to an addition on the right by y + x.

@[simp]
theorem comp_mul_right {α : Type u_1} [Semigroup α] (x : α) (y : α) :
((fun (x_1 : α) => x_1 * x) fun (x : α) => x * y) = fun (x_1 : α) => x_1 * (y * x)

Composing two multiplications on the right by y and x is equal to a multiplication on the right by y * x.

instance AddCommMagma.to_isCommutative {G : Type u_3} [AddCommMagma G] :
Std.Commutative fun (x x_1 : G) => x + x_1
Equations
  • =
instance CommMagma.to_isCommutative {G : Type u_3} [CommMagma G] :
Std.Commutative fun (x x_1 : G) => x * x_1
Equations
  • =
theorem ite_add_zero {M : Type u} [AddZeroClass M] {P : Prop} [Decidable P] {a : M} {b : M} :
(if P then a + b else 0) = (if P then a else 0) + if P then b else 0
theorem ite_mul_one {M : Type u} [MulOneClass M] {P : Prop} [Decidable P] {a : M} {b : M} :
(if P then a * b else 1) = (if P then a else 1) * if P then b else 1
theorem ite_zero_add {M : Type u} [AddZeroClass M] {P : Prop} [Decidable P] {a : M} {b : M} :
(if P then 0 else a + b) = (if P then 0 else a) + if P then 0 else b
theorem ite_one_mul {M : Type u} [MulOneClass M] {P : Prop} [Decidable P] {a : M} {b : M} :
(if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
theorem eq_zero_iff_eq_zero_of_add_eq_zero {M : Type u} [AddZeroClass M] {a : M} {b : M} (h : a + b = 0) :
a = 0 b = 0
theorem eq_one_iff_eq_one_of_mul_eq_one {M : Type u} [MulOneClass M] {a : M} {b : M} (h : a * b = 1) :
a = 1 b = 1
theorem zero_add_eq_id {M : Type u} [AddZeroClass M] :
(fun (x : M) => 0 + x) = id
theorem one_mul_eq_id {M : Type u} [MulOneClass M] :
(fun (x : M) => 1 * x) = id
theorem add_zero_eq_id {M : Type u} [AddZeroClass M] :
(fun (x : M) => x + 0) = id
theorem mul_one_eq_id {M : Type u} [MulOneClass M] :
(fun (x : M) => x * 1) = id
theorem add_left_comm {G : Type u_3} [AddCommSemigroup G] (a : G) (b : G) (c : G) :
a + (b + c) = b + (a + c)
theorem mul_left_comm {G : Type u_3} [CommSemigroup G] (a : G) (b : G) (c : G) :
a * (b * c) = b * (a * c)
theorem add_right_comm {G : Type u_3} [AddCommSemigroup G] (a : G) (b : G) (c : G) :
a + b + c = a + c + b
theorem mul_right_comm {G : Type u_3} [CommSemigroup G] (a : G) (b : G) (c : G) :
a * b * c = a * c * b
theorem add_add_add_comm {G : Type u_3} [AddCommSemigroup G] (a : G) (b : G) (c : G) (d : G) :
a + b + (c + d) = a + c + (b + d)
theorem mul_mul_mul_comm {G : Type u_3} [CommSemigroup G] (a : G) (b : G) (c : G) (d : G) :
a * b * (c * d) = a * c * (b * d)
theorem add_rotate {G : Type u_3} [AddCommSemigroup G] (a : G) (b : G) (c : G) :
a + b + c = b + c + a
theorem mul_rotate {G : Type u_3} [CommSemigroup G] (a : G) (b : G) (c : G) :
a * b * c = b * c * a
theorem add_rotate' {G : Type u_3} [AddCommSemigroup G] (a : G) (b : G) (c : G) :
a + (b + c) = b + (c + a)
theorem mul_rotate' {G : Type u_3} [CommSemigroup G] (a : G) (b : G) (c : G) :
a * (b * c) = b * (c * a)
theorem boole_nsmul {M : Type u_4} [AddMonoid M] (P : Prop) [Decidable P] (a : M) :
(if P then 1 else 0) a = if P then a else 0
theorem pow_boole {M : Type u_4} [Monoid M] (P : Prop) [Decidable P] (a : M) :
(a ^ if P then 1 else 0) = if P then a else 1
theorem nsmul_add_sub_nsmul {M : Type u_4} [AddMonoid M] {m : } {n : } (a : M) (h : m n) :
m a + (n - m) a = n a
theorem pow_mul_pow_sub {M : Type u_4} [Monoid M] {m : } {n : } (a : M) (h : m n) :
a ^ m * a ^ (n - m) = a ^ n
theorem sub_nsmul_nsmul_add {M : Type u_4} [AddMonoid M] {m : } {n : } (a : M) (h : m n) :
(n - m) a + m a = n a
theorem pow_sub_mul_pow {M : Type u_4} [Monoid M] {m : } {n : } (a : M) (h : m n) :
a ^ (n - m) * a ^ m = a ^ n
theorem sub_one_nsmul_add {M : Type u_4} [AddMonoid M] {n : } (hn : n 0) (a : M) :
a + (n - 1) a = n a
theorem mul_pow_sub_one {M : Type u_4} [Monoid M] {n : } (hn : n 0) (a : M) :
a * a ^ (n - 1) = a ^ n
theorem add_sub_one_nsmul {M : Type u_4} [AddMonoid M] {n : } (hn : n 0) (a : M) :
(n - 1) a + a = n a
theorem pow_sub_one_mul {M : Type u_4} [Monoid M] {n : } (hn : n 0) (a : M) :
a ^ (n - 1) * a = a ^ n
theorem nsmul_eq_mod_nsmul {M : Type u_4} [AddMonoid M] {a : M} {n : } (m : ) (ha : n a = 0) :
m a = (m % n) a

If n • x = 0, then m • x is the same as (m % n) • x

theorem pow_eq_pow_mod {M : Type u_4} [Monoid M] {a : M} {n : } (m : ) (ha : a ^ n = 1) :
a ^ m = a ^ (m % n)

If x ^ n = 1, then x ^ m is the same as x ^ (m % n)

abbrev nsmul_add_nsmul_eq_zero.match_1 {M : Type u_1} [AddMonoid M] {a : M} {b : M} (motive : a + b = 0Prop) :
∀ (x : ) (x_1 : a + b = 0), (∀ (x : a + b = 0), motive 0 x)(∀ (n : ) (h : a + b = 0), motive n.succ h)motive x x_1
Equations
  • =
Instances For
    theorem nsmul_add_nsmul_eq_zero {M : Type u_4} [AddMonoid M] {a : M} {b : M} (n : ) :
    a + b = 0n a + n b = 0
    theorem pow_mul_pow_eq_one {M : Type u_4} [Monoid M] {a : M} {b : M} (n : ) :
    a * b = 1a ^ n * b ^ n = 1
    theorem neg_unique {M : Type u_4} [AddCommMonoid M] {x : M} {y : M} {z : M} (hy : x + y = 0) (hz : x + z = 0) :
    y = z
    theorem inv_unique {M : Type u_4} [CommMonoid M] {x : M} {y : M} {z : M} (hy : x * y = 1) (hz : x * z = 1) :
    y = z
    abbrev nsmul_add.match_1 (motive : Prop) :
    ∀ (x : ), (Unitmotive 0)(∀ (n : ), motive n.succ)motive x
    Equations
    • =
    Instances For
      theorem nsmul_add {M : Type u_4} [AddCommMonoid M] (a : M) (b : M) (n : ) :
      n (a + b) = n a + n b
      theorem mul_pow {M : Type u_4} [CommMonoid M] (a : M) (b : M) (n : ) :
      (a * b) ^ n = a ^ n * b ^ n
      @[simp]
      theorem add_right_eq_self {M : Type u} [AddLeftCancelMonoid M] {a : M} {b : M} :
      a + b = a b = 0
      @[simp]
      theorem mul_right_eq_self {M : Type u} [LeftCancelMonoid M] {a : M} {b : M} :
      a * b = a b = 1
      @[simp]
      theorem self_eq_add_right {M : Type u} [AddLeftCancelMonoid M] {a : M} {b : M} :
      a = a + b b = 0
      @[simp]
      theorem self_eq_mul_right {M : Type u} [LeftCancelMonoid M] {a : M} {b : M} :
      a = a * b b = 1
      theorem add_right_ne_self {M : Type u} [AddLeftCancelMonoid M] {a : M} {b : M} :
      a + b a b 0
      theorem mul_right_ne_self {M : Type u} [LeftCancelMonoid M] {a : M} {b : M} :
      a * b a b 1
      theorem self_ne_add_right {M : Type u} [AddLeftCancelMonoid M] {a : M} {b : M} :
      a a + b b 0
      theorem self_ne_mul_right {M : Type u} [LeftCancelMonoid M] {a : M} {b : M} :
      a a * b b 1
      @[simp]
      theorem add_left_eq_self {M : Type u} [AddRightCancelMonoid M] {a : M} {b : M} :
      a + b = b a = 0
      @[simp]
      theorem mul_left_eq_self {M : Type u} [RightCancelMonoid M] {a : M} {b : M} :
      a * b = b a = 1
      @[simp]
      theorem self_eq_add_left {M : Type u} [AddRightCancelMonoid M] {a : M} {b : M} :
      b = a + b a = 0
      @[simp]
      theorem self_eq_mul_left {M : Type u} [RightCancelMonoid M] {a : M} {b : M} :
      b = a * b a = 1
      theorem add_left_ne_self {M : Type u} [AddRightCancelMonoid M] {a : M} {b : M} :
      a + b b a 0
      theorem mul_left_ne_self {M : Type u} [RightCancelMonoid M] {a : M} {b : M} :
      a * b b a 1
      theorem self_ne_add_left {M : Type u} [AddRightCancelMonoid M] {a : M} {b : M} :
      b a + b a 0
      theorem self_ne_mul_left {M : Type u} [RightCancelMonoid M] {a : M} {b : M} :
      b a * b a 1
      theorem eq_iff_eq_of_add_eq_add {α : Type u_1} [AddCancelCommMonoid α] {a : α} {b : α} {c : α} {d : α} (h : a + b = c + d) :
      a = c b = d
      theorem eq_iff_eq_of_mul_eq_mul {α : Type u_1} [CancelCommMonoid α] {a : α} {b : α} {c : α} {d : α} (h : a * b = c * d) :
      a = c b = d
      theorem ne_iff_ne_of_add_eq_add {α : Type u_1} [AddCancelCommMonoid α] {a : α} {b : α} {c : α} {d : α} (h : a + b = c + d) :
      a c b d
      theorem ne_iff_ne_of_mul_eq_mul {α : Type u_1} [CancelCommMonoid α] {a : α} {b : α} {c : α} {d : α} (h : a * b = c * d) :
      a c b d
      @[simp]
      theorem neg_involutive {G : Type u_3} [InvolutiveNeg G] :
      @[simp]
      theorem inv_involutive {G : Type u_3} [InvolutiveInv G] :
      @[simp]
      theorem neg_surjective {G : Type u_3} [InvolutiveNeg G] :
      @[simp]
      theorem inv_surjective {G : Type u_3} [InvolutiveInv G] :
      @[simp]
      theorem neg_inj {G : Type u_3} [InvolutiveNeg G] {a : G} {b : G} :
      -a = -b a = b
      @[simp]
      theorem inv_inj {G : Type u_3} [InvolutiveInv G] {a : G} {b : G} :
      a⁻¹ = b⁻¹ a = b
      theorem neg_eq_iff_eq_neg {G : Type u_3} [InvolutiveNeg G] {a : G} {b : G} :
      -a = b a = -b
      theorem inv_eq_iff_eq_inv {G : Type u_3} [InvolutiveInv G] {a : G} {b : G} :
      a⁻¹ = b a = b⁻¹
      theorem neg_comp_neg (G : Type u_3) [InvolutiveNeg G] :
      Neg.neg Neg.neg = id
      theorem inv_comp_inv (G : Type u_3) [InvolutiveInv G] :
      Inv.inv Inv.inv = id
      theorem leftInverse_neg (G : Type u_3) [InvolutiveNeg G] :
      Function.LeftInverse (fun (a : G) => -a) fun (a : G) => -a
      theorem leftInverse_inv (G : Type u_3) [InvolutiveInv G] :
      Function.LeftInverse (fun (a : G) => a⁻¹) fun (a : G) => a⁻¹
      theorem rightInverse_neg (G : Type u_3) [InvolutiveNeg G] :
      Function.RightInverse (fun (a : G) => -a) fun (a : G) => -a
      theorem rightInverse_inv (G : Type u_3) [InvolutiveInv G] :
      Function.RightInverse (fun (a : G) => a⁻¹) fun (a : G) => a⁻¹
      theorem neg_eq_zero_sub {G : Type u_3} [SubNegMonoid G] (x : G) :
      -x = 0 - x
      theorem inv_eq_one_div {G : Type u_3} [DivInvMonoid G] (x : G) :
      x⁻¹ = 1 / x
      theorem add_zero_sub {G : Type u_3} [SubNegMonoid G] (x : G) (y : G) :
      x + (0 - y) = x - y
      theorem mul_one_div {G : Type u_3} [DivInvMonoid G] (x : G) (y : G) :
      x * (1 / y) = x / y
      theorem add_sub_assoc {G : Type u_3} [SubNegMonoid G] (a : G) (b : G) (c : G) :
      a + b - c = a + (b - c)
      theorem mul_div_assoc {G : Type u_3} [DivInvMonoid G] (a : G) (b : G) (c : G) :
      a * b / c = a * (b / c)
      theorem add_sub_assoc' {G : Type u_3} [SubNegMonoid G] (a : G) (b : G) (c : G) :
      a + (b - c) = a + b - c
      theorem mul_div_assoc' {G : Type u_3} [DivInvMonoid G] (a : G) (b : G) (c : G) :
      a * (b / c) = a * b / c
      @[simp]
      theorem zero_sub {G : Type u_3} [SubNegMonoid G] (a : G) :
      0 - a = -a
      @[simp]
      theorem one_div {G : Type u_3} [DivInvMonoid G] (a : G) :
      1 / a = a⁻¹
      theorem add_sub {G : Type u_3} [SubNegMonoid G] (a : G) (b : G) (c : G) :
      a + (b - c) = a + b - c
      theorem mul_div {G : Type u_3} [DivInvMonoid G] (a : G) (b : G) (c : G) :
      a * (b / c) = a * b / c
      theorem sub_eq_add_zero_sub {G : Type u_3} [SubNegMonoid G] (a : G) (b : G) :
      a - b = a + (0 - b)
      theorem div_eq_mul_one_div {G : Type u_3} [DivInvMonoid G] (a : G) (b : G) :
      a / b = a * (1 / b)
      @[simp]
      theorem sub_zero {G : Type u_3} [SubNegZeroMonoid G] (a : G) :
      a - 0 = a
      @[simp]
      theorem div_one {G : Type u_3} [DivInvOneMonoid G] (a : G) :
      a / 1 = a
      theorem zero_sub_zero {G : Type u_3} [SubNegZeroMonoid G] :
      0 - 0 = 0
      theorem one_div_one {G : Type u_3} [DivInvOneMonoid G] :
      1 / 1 = 1
      theorem eq_neg_of_add_eq_zero_right {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} (h : a + b = 0) :
      b = -a
      theorem eq_inv_of_mul_eq_one_right {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : a * b = 1) :
      b = a⁻¹
      theorem eq_zero_sub_of_add_eq_zero_left {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} (h : b + a = 0) :
      b = 0 - a
      theorem eq_one_div_of_mul_eq_one_left {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : b * a = 1) :
      b = 1 / a
      theorem eq_zero_sub_of_add_eq_zero_right {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} (h : a + b = 0) :
      b = 0 - a
      theorem eq_one_div_of_mul_eq_one_right {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : a * b = 1) :
      b = 1 / a
      theorem eq_of_sub_eq_zero {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} (h : a - b = 0) :
      a = b
      theorem eq_of_div_eq_one {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : a / b = 1) :
      a = b
      theorem eq_of_inv_mul_eq_one {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : a⁻¹ * b = 1) :
      a = b
      theorem eq_of_mul_inv_eq_one {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : a * b⁻¹ = 1) :
      a = b
      theorem sub_ne_zero_of_ne {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} :
      a ba - b 0
      theorem div_ne_one_of_ne {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} :
      a ba / b 1
      theorem zero_sub_add_zero_sub_rev {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) :
      0 - a + (0 - b) = 0 - (b + a)
      theorem one_div_mul_one_div_rev {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) :
      1 / a * (1 / b) = 1 / (b * a)
      theorem neg_sub_left {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) :
      -a - b = -(b + a)
      theorem inv_div_left {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) :
      a⁻¹ / b = (b * a)⁻¹
      @[simp]
      theorem neg_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) :
      -(a - b) = b - a
      @[simp]
      theorem inv_div {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) :
      (a / b)⁻¹ = b / a
      theorem zero_sub_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) :
      0 - (a - b) = b - a
      theorem one_div_div {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) :
      1 / (a / b) = b / a
      theorem zero_sub_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) :
      0 - (0 - a) = a
      theorem one_div_one_div {α : Type u_1} [DivisionMonoid α] (a : α) :
      1 / (1 / a) = a
      theorem sub_eq_sub_iff_comm {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) (c : α) {d : α} :
      a - b = c - d b - a = d - c
      theorem div_eq_div_iff_comm {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) (c : α) {d : α} :
      a / b = c / d b / a = d / c
      @[instance 100]
      Equations
      • SubtractionMonoid.toSubNegZeroMonoid = let __src := SubtractionMonoid.toSubNegMonoid; SubNegZeroMonoid.mk
      @[instance 100]
      Equations
      • DivisionMonoid.toDivInvOneMonoid = let __src := DivisionMonoid.toDivInvMonoid; DivInvOneMonoid.mk
      @[simp]
      theorem neg_nsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ) :
      n -a = -(n a)
      @[simp]
      theorem inv_pow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ) :
      a⁻¹ ^ n = (a ^ n)⁻¹
      abbrev zsmul_zero.match_1 (motive : Prop) :
      ∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(∀ (n : ), motive (Int.negSucc n))motive x
      Equations
      • =
      Instances For
        theorem zsmul_zero {α : Type u_1} [SubtractionMonoid α] (n : ) :
        n 0 = 0
        @[simp]
        theorem one_zpow {α : Type u_1} [DivisionMonoid α] (n : ) :
        1 ^ n = 1
        @[simp]
        theorem neg_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ) :
        -n a = -(n a)
        abbrev neg_zsmul.match_1 (motive : Prop) :
        ∀ (x : ), (∀ (n : ), motive (Int.ofNat n.succ))(Unitmotive 0)(∀ (n : ), motive (Int.negSucc n))motive x
        Equations
        • =
        Instances For
          @[simp]
          theorem zpow_neg {α : Type u_1} [DivisionMonoid α] (a : α) (n : ) :
          a ^ (-n) = (a ^ n)⁻¹
          theorem neg_one_zsmul_add {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) :
          -1 (a + b) = -1 b + -1 a
          theorem mul_zpow_neg_one {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) :
          (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
          theorem zsmul_neg {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ) :
          n -a = -(n a)
          theorem inv_zpow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ) :
          a⁻¹ ^ n = (a ^ n)⁻¹
          @[simp]
          theorem zsmul_neg' {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ) :
          n -a = -n a
          @[simp]
          theorem inv_zpow' {α : Type u_1} [DivisionMonoid α] (a : α) (n : ) :
          a⁻¹ ^ n = a ^ (-n)
          theorem nsmul_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ) :
          n (0 - a) = 0 - n a
          theorem one_div_pow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ) :
          (1 / a) ^ n = 1 / a ^ n
          theorem zsmul_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ) :
          n (0 - a) = 0 - n a
          theorem one_div_zpow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ) :
          (1 / a) ^ n = 1 / a ^ n
          @[simp]
          theorem neg_eq_zero {α : Type u_1} [SubtractionMonoid α] {a : α} :
          -a = 0 a = 0
          @[simp]
          theorem inv_eq_one {α : Type u_1} [DivisionMonoid α] {a : α} :
          a⁻¹ = 1 a = 1
          @[simp]
          theorem zero_eq_neg {α : Type u_1} [SubtractionMonoid α] {a : α} :
          0 = -a a = 0
          @[simp]
          theorem one_eq_inv {α : Type u_1} [DivisionMonoid α] {a : α} :
          1 = a⁻¹ a = 1
          theorem neg_ne_zero {α : Type u_1} [SubtractionMonoid α] {a : α} :
          -a 0 a 0
          theorem inv_ne_one {α : Type u_1} [DivisionMonoid α] {a : α} :
          a⁻¹ 1 a 1
          theorem eq_of_zero_sub_eq_zero_sub {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} (h : 0 - a = 0 - b) :
          a = b
          theorem eq_of_one_div_eq_one_div {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : 1 / a = 1 / b) :
          a = b
          theorem mul_zsmul' {α : Type u_1} [SubtractionMonoid α] (a : α) (m : ) (n : ) :
          (m * n) a = n m a
          abbrev mul_zsmul'.match_1 (motive : Prop) :
          ∀ (x x_1 : ), (∀ (m n : ), motive (Int.ofNat m) (Int.ofNat n))(∀ (m n : ), motive (Int.ofNat m) (Int.negSucc n))(∀ (m n : ), motive (Int.negSucc m) (Int.ofNat n))(∀ (m n : ), motive (Int.negSucc m) (Int.negSucc n))motive x x_1
          Equations
          • =
          Instances For
            theorem zpow_mul {α : Type u_1} [DivisionMonoid α] (a : α) (m : ) (n : ) :
            a ^ (m * n) = (a ^ m) ^ n
            theorem mul_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (m : ) (n : ) :
            (m * n) a = m n a
            theorem zpow_mul' {α : Type u_1} [DivisionMonoid α] (a : α) (m : ) (n : ) :
            a ^ (m * n) = (a ^ n) ^ m
            theorem sub_sub_eq_add_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) (c : α) :
            a - (b - c) = a + c - b
            theorem div_div_eq_mul_div {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) (c : α) :
            a / (b / c) = a * c / b
            @[simp]
            theorem sub_neg_eq_add {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) :
            a - -b = a + b
            @[simp]
            theorem div_inv_eq_mul {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) :
            a / b⁻¹ = a * b
            theorem sub_add_eq_sub_sub_swap {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) (c : α) :
            a - (b + c) = a - c - b
            theorem div_mul_eq_div_div_swap {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) (c : α) :
            a / (b * c) = a / c / b
            theorem neg_add {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            -(a + b) = -a + -b
            theorem mul_inv {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            (a * b)⁻¹ = a⁻¹ * b⁻¹
            theorem neg_sub' {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            -(a - b) = -a - -b
            theorem inv_div' {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            (a / b)⁻¹ = a⁻¹ / b⁻¹
            theorem sub_eq_neg_add {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            a - b = -b + a
            theorem div_eq_inv_mul {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            a / b = b⁻¹ * a
            theorem neg_add_eq_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            -a + b = b - a
            theorem inv_mul_eq_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            a⁻¹ * b = b / a
            theorem neg_add' {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            -(a + b) = -a - b
            theorem inv_mul' {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            (a * b)⁻¹ = a⁻¹ / b
            theorem neg_sub_neg {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            -a - -b = b - a
            theorem inv_div_inv {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            a⁻¹ / b⁻¹ = b / a
            theorem neg_neg_sub_neg {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            -(-a - -b) = a - b
            theorem inv_inv_div_inv {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            (a⁻¹ / b⁻¹)⁻¹ = a / b
            theorem zero_sub_add_zero_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            0 - a + (0 - b) = 0 - (a + b)
            theorem one_div_mul_one_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            1 / a * (1 / b) = 1 / (a * b)
            theorem sub_right_comm {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - b - c = a - c - b
            theorem div_right_comm {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / b / c = a / c / b
            theorem sub_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - b - c = a - (b + c)
            theorem div_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / b / c = a / (b * c)
            theorem sub_add {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - b + c = a - (b - c)
            theorem div_mul {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / b * c = a / (b / c)
            theorem add_sub_left_comm {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a + (b - c) = b + (a - c)
            theorem mul_div_left_comm {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a * (b / c) = b * (a / c)
            theorem add_sub_right_comm {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a + b - c = a - c + b
            theorem mul_div_right_comm {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a * b / c = a / c * b
            theorem sub_add_eq_sub_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - (b + c) = a - b - c
            theorem div_mul_eq_div_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / (b * c) = a / b / c
            theorem sub_add_eq_add_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - b + c = a + c - b
            theorem div_mul_eq_mul_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / b * c = a * c / b
            theorem zero_sub_add_eq_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) :
            0 - a + b = b - a
            theorem one_div_mul_eq_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) :
            1 / a * b = b / a
            theorem add_comm_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - b + c = a + (c - b)
            theorem mul_comm_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / b * c = a * (c / b)
            theorem sub_add_comm {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - b + c = c - b + a
            theorem div_mul_comm {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / b * c = c / b * a
            theorem sub_add_eq_sub_add_zero_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) :
            a - (b + c) = a - b + (0 - c)
            theorem div_mul_eq_div_mul_one_div {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) :
            a / (b * c) = a / b * (1 / c)
            theorem sub_sub_sub_eq {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a - b - (c - d) = a + d - (b + c)
            theorem div_div_div_eq {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a / b / (c / d) = a * d / (b * c)
            theorem sub_sub_sub_comm {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a - b - (c - d) = a - c - (b - d)
            theorem div_div_div_comm {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a / b / (c / d) = a / c / (b / d)
            theorem sub_add_sub_comm {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a - b + (c - d) = a + c - (b + d)
            theorem div_mul_div_comm {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a / b * (c / d) = a * c / (b * d)
            theorem add_sub_add_comm {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a + b - (c + d) = a - c + (b - d)
            theorem mul_div_mul_comm {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (c : α) (d : α) :
            a * b / (c * d) = a / c * (b / d)
            theorem zsmul_add {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (n : ) :
            n (a + b) = n a + n b
            theorem mul_zpow {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (n : ) :
            (a * b) ^ n = a ^ n * b ^ n
            @[simp]
            theorem nsmul_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (n : ) :
            n (a - b) = n a - n b
            @[simp]
            theorem div_pow {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (n : ) :
            (a / b) ^ n = a ^ n / b ^ n
            @[simp]
            theorem zsmul_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (n : ) :
            n (a - b) = n a - n b
            @[simp]
            theorem div_zpow {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (n : ) :
            (a / b) ^ n = a ^ n / b ^ n
            @[simp]
            theorem sub_eq_neg_self {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a - b = -b a = 0
            @[simp]
            theorem div_eq_inv_self {G : Type u_3} [Group G] {a : G} {b : G} :
            a / b = b⁻¹ a = 1
            theorem add_left_surjective {G : Type u_3} [AddGroup G] (a : G) :
            Function.Surjective fun (x : G) => a + x
            theorem mul_left_surjective {G : Type u_3} [Group G] (a : G) :
            Function.Surjective fun (x : G) => a * x
            theorem add_right_surjective {G : Type u_3} [AddGroup G] (a : G) :
            Function.Surjective fun (x : G) => x + a
            theorem mul_right_surjective {G : Type u_3} [Group G] (a : G) :
            Function.Surjective fun (x : G) => x * a
            theorem eq_add_neg_of_add_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a + c = b) :
            a = b + -c
            theorem eq_mul_inv_of_mul_eq {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a * c = b) :
            a = b * c⁻¹
            theorem eq_neg_add_of_add_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : b + a = c) :
            a = -b + c
            theorem eq_inv_mul_of_mul_eq {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : b * a = c) :
            a = b⁻¹ * c
            theorem neg_add_eq_of_eq_add {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : b = a + c) :
            -a + b = c
            theorem inv_mul_eq_of_eq_mul {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : b = a * c) :
            a⁻¹ * b = c
            theorem add_neg_eq_of_eq_add {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a = c + b) :
            a + -b = c
            theorem mul_inv_eq_of_eq_mul {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a = c * b) :
            a * b⁻¹ = c
            theorem eq_add_of_add_neg_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a + -c = b) :
            a = b + c
            theorem eq_mul_of_mul_inv_eq {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a * c⁻¹ = b) :
            a = b * c
            theorem eq_add_of_neg_add_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : -b + a = c) :
            a = b + c
            theorem eq_mul_of_inv_mul_eq {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : b⁻¹ * a = c) :
            a = b * c
            theorem add_eq_of_eq_neg_add {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : b = -a + c) :
            a + b = c
            theorem mul_eq_of_eq_inv_mul {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : b = a⁻¹ * c) :
            a * b = c
            theorem add_eq_of_eq_add_neg {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a = c + -b) :
            a + b = c
            theorem mul_eq_of_eq_mul_inv {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a = c * b⁻¹) :
            a * b = c
            theorem add_eq_zero_iff_eq_neg {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a + b = 0 a = -b
            theorem mul_eq_one_iff_eq_inv {G : Type u_3} [Group G] {a : G} {b : G} :
            a * b = 1 a = b⁻¹
            theorem add_eq_zero_iff_neg_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a + b = 0 -a = b
            theorem mul_eq_one_iff_inv_eq {G : Type u_3} [Group G] {a : G} {b : G} :
            a * b = 1 a⁻¹ = b
            theorem eq_neg_iff_add_eq_zero {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a = -b a + b = 0
            theorem eq_inv_iff_mul_eq_one {G : Type u_3} [Group G] {a : G} {b : G} :
            a = b⁻¹ a * b = 1
            theorem neg_eq_iff_add_eq_zero {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            -a = b a + b = 0
            theorem inv_eq_iff_mul_eq_one {G : Type u_3} [Group G] {a : G} {b : G} :
            a⁻¹ = b a * b = 1
            theorem eq_add_neg_iff_add_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            a = b + -c a + c = b
            theorem eq_mul_inv_iff_mul_eq {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            a = b * c⁻¹ a * c = b
            theorem eq_neg_add_iff_add_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            a = -b + c b + a = c
            theorem eq_inv_mul_iff_mul_eq {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            a = b⁻¹ * c b * a = c
            theorem neg_add_eq_iff_eq_add {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            -a + b = c b = a + c
            theorem inv_mul_eq_iff_eq_mul {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            a⁻¹ * b = c b = a * c
            theorem add_neg_eq_iff_eq_add {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            a + -b = c a = c + b
            theorem mul_inv_eq_iff_eq_mul {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            a * b⁻¹ = c a = c * b
            theorem add_neg_eq_zero {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a + -b = 0 a = b
            theorem mul_inv_eq_one {G : Type u_3} [Group G] {a : G} {b : G} :
            a * b⁻¹ = 1 a = b
            theorem neg_add_eq_zero {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            -a + b = 0 a = b
            theorem inv_mul_eq_one {G : Type u_3} [Group G] {a : G} {b : G} :
            a⁻¹ * b = 1 a = b
            @[simp]
            theorem conj_eq_zero_iff {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a + b + -a = 0 b = 0
            @[simp]
            theorem conj_eq_one_iff {G : Type u_3} [Group G] {a : G} {b : G} :
            a * b * a⁻¹ = 1 b = 1
            theorem sub_left_injective {G : Type u_3} [AddGroup G] {b : G} :
            Function.Injective fun (a : G) => a - b
            theorem div_left_injective {G : Type u_3} [Group G] {b : G} :
            Function.Injective fun (a : G) => a / b
            theorem sub_right_injective {G : Type u_3} [AddGroup G] {b : G} :
            Function.Injective fun (a : G) => b - a
            theorem div_right_injective {G : Type u_3} [Group G] {b : G} :
            Function.Injective fun (a : G) => b / a
            @[simp]
            theorem sub_add_cancel {G : Type u_3} [AddGroup G] (a : G) (b : G) :
            a - b + b = a
            @[simp]
            theorem div_mul_cancel {G : Type u_3} [Group G] (a : G) (b : G) :
            a / b * b = a
            @[simp]
            theorem sub_self {G : Type u_3} [AddGroup G] (a : G) :
            a - a = 0
            @[simp]
            theorem div_self' {G : Type u_3} [Group G] (a : G) :
            a / a = 1
            @[simp]
            theorem add_sub_cancel_right {G : Type u_3} [AddGroup G] (a : G) (b : G) :
            a + b - b = a
            @[simp]
            theorem mul_div_cancel_right {G : Type u_3} [Group G] (a : G) (b : G) :
            a * b / b = a
            @[simp]
            theorem sub_add_cancel_right {G : Type u_3} [AddGroup G] (a : G) (b : G) :
            a - (b + a) = -b
            @[simp]
            theorem div_mul_cancel_right {G : Type u_3} [Group G] (a : G) (b : G) :
            a / (b * a) = b⁻¹
            @[simp]
            theorem add_sub_add_right_eq_sub {G : Type u_3} [AddGroup G] (a : G) (b : G) (c : G) :
            a + c - (b + c) = a - b
            @[simp]
            theorem mul_div_mul_right_eq_div {G : Type u_3} [Group G] (a : G) (b : G) (c : G) :
            a * c / (b * c) = a / b
            theorem eq_sub_of_add_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a + c = b) :
            a = b - c
            theorem eq_div_of_mul_eq' {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a * c = b) :
            a = b / c
            theorem sub_eq_of_eq_add {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a = c + b) :
            a - b = c
            theorem div_eq_of_eq_mul'' {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a = c * b) :
            a / b = c
            theorem eq_add_of_sub_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a - c = b) :
            a = b + c
            theorem eq_mul_of_div_eq {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a / c = b) :
            a = b * c
            theorem add_eq_of_eq_sub {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} (h : a = c - b) :
            a + b = c
            theorem mul_eq_of_eq_div {G : Type u_3} [Group G] {a : G} {b : G} {c : G} (h : a = c / b) :
            a * b = c
            @[simp]
            theorem sub_right_inj {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            a - b = a - c b = c
            @[simp]
            theorem div_right_inj {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            a / b = a / c b = c
            @[simp]
            theorem sub_left_inj {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            b - a = c - a b = c
            @[simp]
            theorem div_left_inj {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            b / a = c / a b = c
            @[simp]
            theorem sub_add_sub_cancel {G : Type u_3} [AddGroup G] (a : G) (b : G) (c : G) :
            a - b + (b - c) = a - c
            @[simp]
            theorem div_mul_div_cancel' {G : Type u_3} [Group G] (a : G) (b : G) (c : G) :
            a / b * (b / c) = a / c
            @[simp]
            theorem sub_sub_sub_cancel_right {G : Type u_3} [AddGroup G] (a : G) (b : G) (c : G) :
            a - c - (b - c) = a - b
            @[simp]
            theorem div_div_div_cancel_right' {G : Type u_3} [Group G] (a : G) (b : G) (c : G) :
            a / c / (b / c) = a / b
            theorem sub_eq_zero {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a - b = 0 a = b
            theorem div_eq_one {G : Type u_3} [Group G] {a : G} {b : G} :
            a / b = 1 a = b
            theorem div_eq_one_of_eq {G : Type u_3} [Group G] {a : G} {b : G} :
            a = ba / b = 1

            Alias of the reverse direction of div_eq_one.

            theorem sub_eq_zero_of_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a = ba - b = 0

            Alias of the reverse direction of sub_eq_zero.

            theorem sub_ne_zero {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a - b 0 a b
            theorem div_ne_one {G : Type u_3} [Group G] {a : G} {b : G} :
            a / b 1 a b
            @[simp]
            theorem sub_eq_self {G : Type u_3} [AddGroup G] {a : G} {b : G} :
            a - b = a b = 0
            @[simp]
            theorem div_eq_self {G : Type u_3} [Group G] {a : G} {b : G} :
            a / b = a b = 1
            theorem eq_sub_iff_add_eq {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            a = b - c a + c = b
            theorem eq_div_iff_mul_eq' {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            a = b / c a * c = b
            theorem sub_eq_iff_eq_add {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} :
            a - b = c a = c + b
            theorem div_eq_iff_eq_mul {G : Type u_3} [Group G] {a : G} {b : G} {c : G} :
            a / b = c a = c * b
            theorem eq_iff_eq_of_sub_eq_sub {G : Type u_3} [AddGroup G] {a : G} {b : G} {c : G} {d : G} (H : a - b = c - d) :
            a = b c = d
            theorem eq_iff_eq_of_div_eq_div {G : Type u_3} [Group G] {a : G} {b : G} {c : G} {d : G} (H : a / b = c / d) :
            a = b c = d
            theorem leftInverse_sub_add_left {G : Type u_3} [AddGroup G] (c : G) :
            Function.LeftInverse (fun (x : G) => x - c) fun (x : G) => x + c
            theorem leftInverse_div_mul_left {G : Type u_3} [Group G] (c : G) :
            Function.LeftInverse (fun (x : G) => x / c) fun (x : G) => x * c
            theorem leftInverse_add_left_sub {G : Type u_3} [AddGroup G] (c : G) :
            Function.LeftInverse (fun (x : G) => x + c) fun (x : G) => x - c
            theorem leftInverse_mul_left_div {G : Type u_3} [Group G] (c : G) :
            Function.LeftInverse (fun (x : G) => x * c) fun (x : G) => x / c
            theorem leftInverse_add_right_neg_add {G : Type u_3} [AddGroup G] (c : G) :
            Function.LeftInverse (fun (x : G) => c + x) fun (x : G) => -c + x
            theorem leftInverse_mul_right_inv_mul {G : Type u_3} [Group G] (c : G) :
            Function.LeftInverse (fun (x : G) => c * x) fun (x : G) => c⁻¹ * x
            theorem leftInverse_neg_add_add_right {G : Type u_3} [AddGroup G] (c : G) :
            Function.LeftInverse (fun (x : G) => -c + x) fun (x : G) => c + x
            theorem leftInverse_inv_mul_mul_right {G : Type u_3} [Group G] (c : G) :
            Function.LeftInverse (fun (x : G) => c⁻¹ * x) fun (x : G) => c * x
            @[simp]
            theorem natAbs_nsmul_eq_zero {G : Type u_3} [AddGroup G] {a : G} {n : } :
            n.natAbs a = 0 n a = 0
            @[simp]
            theorem pow_natAbs_eq_one {G : Type u_3} [Group G] {a : G} {n : } :
            a ^ n.natAbs = 1 a ^ n = 1
            @[deprecated natAbs_nsmul_eq_zero]
            theorem exists_nsmul_eq_zero_of_zsmul_eq_zero {G : Type u_3} [AddGroup G] {a : G} {n : } (hn : n 0) (h : n a = 0) :
            ∃ (n : ), 0 < n n a = 0
            @[deprecated pow_natAbs_eq_one]
            theorem exists_pow_eq_one_of_zpow_eq_one {G : Type u_3} [Group G] {a : G} {n : } (hn : n 0) (h : a ^ n = 1) :
            ∃ (n : ), 0 < n a ^ n = 1
            theorem sub_nsmul {G : Type u_3} [AddGroup G] (a : G) {m : } {n : } (h : n m) :
            (m - n) a = m a + -(n a)
            theorem pow_sub {G : Type u_3} [Group G] (a : G) {m : } {n : } (h : n m) :
            a ^ (m - n) = a ^ m * (a ^ n)⁻¹
            theorem sub_nsmul_neg {G : Type u_3} [AddGroup G] (a : G) {m : } {n : } (h : n m) :
            (m - n) -a = -(m a) + n a
            theorem inv_pow_sub {G : Type u_3} [Group G] (a : G) {m : } {n : } (h : n m) :
            a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
            theorem add_one_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ) :
            (n + 1) a = n a + a
            abbrev add_one_zsmul.match_1 (motive : Prop) :
            ∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(Unitmotive (Int.negSucc 0))(∀ (n : ), motive (Int.negSucc n.succ))motive x
            Equations
            • =
            Instances For
              theorem zpow_add_one {G : Type u_3} [Group G] (a : G) (n : ) :
              a ^ (n + 1) = a ^ n * a
              theorem sub_one_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ) :
              (n - 1) a = n a + -a
              theorem zpow_sub_one {G : Type u_3} [Group G] (a : G) (n : ) :
              a ^ (n - 1) = a ^ n * a⁻¹
              theorem add_zsmul {G : Type u_3} [AddGroup G] (a : G) (m : ) (n : ) :
              (m + n) a = m a + n a
              theorem zpow_add {G : Type u_3} [Group G] (a : G) (m : ) (n : ) :
              a ^ (m + n) = a ^ m * a ^ n
              theorem one_add_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ) :
              (1 + n) a = a + n a
              theorem zpow_one_add {G : Type u_3} [Group G] (a : G) (n : ) :
              a ^ (1 + n) = a * a ^ n
              theorem add_zsmul_self {G : Type u_3} [AddGroup G] (a : G) (n : ) :
              a + n a = (n + 1) a
              theorem mul_self_zpow {G : Type u_3} [Group G] (a : G) (n : ) :
              a * a ^ n = a ^ (n + 1)
              theorem add_self_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ) :
              n a + a = (n + 1) a
              theorem mul_zpow_self {G : Type u_3} [Group G] (a : G) (n : ) :
              a ^ n * a = a ^ (n + 1)
              theorem sub_zsmul {G : Type u_3} [AddGroup G] (a : G) (m : ) (n : ) :
              (m - n) a = m a + -(n a)
              theorem zpow_sub {G : Type u_3} [Group G] (a : G) (m : ) (n : ) :
              a ^ (m - n) = a ^ m * (a ^ n)⁻¹
              theorem zsmul_add_comm {G : Type u_3} [AddGroup G] (a : G) (m : ) (n : ) :
              m a + n a = n a + m a
              theorem zpow_mul_comm {G : Type u_3} [Group G] (a : G) (m : ) (n : ) :
              a ^ m * a ^ n = a ^ n * a ^ m
              theorem zpow_eq_zpow_emod {G : Type u_3} [Group G] {x : G} (m : ) {n : } (h : x ^ n = 1) :
              x ^ m = x ^ (m % n)
              theorem zpow_eq_zpow_emod' {G : Type u_3} [Group G] {x : G} (m : ) {n : } (h : x ^ n = 1) :
              x ^ m = x ^ (m % n)
              theorem zsmul_induction_left {G : Type u_3} [AddGroup G] {g : G} {P : GProp} (h_one : P 0) (h_mul : ∀ (a : G), P aP (g + a)) (h_inv : ∀ (a : G), P aP (-g + a)) (n : ) :
              P (n g)

              To show a property of all multiples of g it suffices to show it is closed under addition by g and -g on the left. For additive subgroups generated by more than one element, see AddSubgroup.closure_induction_left.

              theorem zpow_induction_left {G : Type u_3} [Group G] {g : G} {P : GProp} (h_one : P 1) (h_mul : ∀ (a : G), P aP (g * a)) (h_inv : ∀ (a : G), P aP (g⁻¹ * a)) (n : ) :
              P (g ^ n)

              To show a property of all powers of g it suffices to show it is closed under multiplication by g and g⁻¹ on the left. For subgroups generated by more than one element, see Subgroup.closure_induction_left.

              theorem zsmul_induction_right {G : Type u_3} [AddGroup G] {g : G} {P : GProp} (h_one : P 0) (h_mul : ∀ (a : G), P aP (a + g)) (h_inv : ∀ (a : G), P aP (a + -g)) (n : ) :
              P (n g)

              To show a property of all multiples of g it suffices to show it is closed under addition by g and -g on the right. For additive subgroups generated by more than one element, see AddSubgroup.closure_induction_right.

              theorem zpow_induction_right {G : Type u_3} [Group G] {g : G} {P : GProp} (h_one : P 1) (h_mul : ∀ (a : G), P aP (a * g)) (h_inv : ∀ (a : G), P aP (a * g⁻¹)) (n : ) :
              P (g ^ n)

              To show a property of all powers of g it suffices to show it is closed under multiplication by g and g⁻¹ on the right. For subgroups generated by more than one element, see Subgroup.closure_induction_right.

              theorem sub_eq_of_eq_add' {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} (h : a = b + c) :
              a - b = c
              theorem div_eq_of_eq_mul' {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} (h : a = b * c) :
              a / b = c
              @[simp]
              theorem add_sub_add_left_eq_sub {G : Type u_3} [AddCommGroup G] (a : G) (b : G) (c : G) :
              c + a - (c + b) = a - b
              @[simp]
              theorem mul_div_mul_left_eq_div {G : Type u_3} [CommGroup G] (a : G) (b : G) (c : G) :
              c * a / (c * b) = a / b
              theorem eq_sub_of_add_eq' {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} (h : c + a = b) :
              a = b - c
              theorem eq_div_of_mul_eq'' {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} (h : c * a = b) :
              a = b / c
              theorem eq_add_of_sub_eq' {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} (h : a - b = c) :
              a = b + c
              theorem eq_mul_of_div_eq' {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} (h : a / b = c) :
              a = b * c
              theorem add_eq_of_eq_sub' {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} (h : b = c - a) :
              a + b = c
              theorem mul_eq_of_eq_div' {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} (h : b = c / a) :
              a * b = c
              theorem sub_sub_self {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a - (a - b) = b
              theorem div_div_self' {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a / (a / b) = b
              theorem sub_eq_sub_add_sub {G : Type u_3} [AddCommGroup G] (a : G) (b : G) (c : G) :
              a - b = c - b + (a - c)
              theorem div_eq_div_mul_div {G : Type u_3} [CommGroup G] (a : G) (b : G) (c : G) :
              a / b = c / b * (a / c)
              @[simp]
              theorem sub_sub_cancel {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a - (a - b) = b
              @[simp]
              theorem div_div_cancel {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a / (a / b) = b
              @[simp]
              theorem sub_sub_cancel_left {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a - b - a = -b
              @[simp]
              theorem div_div_cancel_left {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a / b / a = b⁻¹
              theorem eq_sub_iff_add_eq' {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} :
              a = b - c c + a = b
              theorem eq_div_iff_mul_eq'' {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} :
              a = b / c c * a = b
              theorem sub_eq_iff_eq_add' {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} :
              a - b = c a = b + c
              theorem div_eq_iff_eq_mul' {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} :
              a / b = c a = b * c
              @[simp]
              theorem add_sub_cancel_left {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a + b - a = b
              @[simp]
              theorem mul_div_cancel_left {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a * b / a = b
              @[simp]
              theorem add_sub_cancel {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a + (b - a) = b
              @[simp]
              theorem mul_div_cancel {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a * (b / a) = b
              @[simp]
              theorem sub_add_cancel_left {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a - (a + b) = -b
              @[simp]
              theorem div_mul_cancel_left {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a / (a * b) = b⁻¹
              theorem add_add_neg_cancel'_right {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a + (b + -a) = b
              theorem mul_mul_inv_cancel'_right {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a * (b * a⁻¹) = b
              @[simp]
              theorem add_add_sub_cancel {G : Type u_3} [AddCommGroup G] (a : G) (b : G) (c : G) :
              a + c + (b - c) = a + b
              @[simp]
              theorem mul_mul_div_cancel {G : Type u_3} [CommGroup G] (a : G) (b : G) (c : G) :
              a * c * (b / c) = a * b
              @[simp]
              theorem sub_add_add_cancel {G : Type u_3} [AddCommGroup G] (a : G) (b : G) (c : G) :
              a - c + (b + c) = a + b
              @[simp]
              theorem div_mul_mul_cancel {G : Type u_3} [CommGroup G] (a : G) (b : G) (c : G) :
              a / c * (b * c) = a * b
              @[simp]
              theorem sub_add_sub_cancel' {G : Type u_3} [AddCommGroup G] (a : G) (b : G) (c : G) :
              a - b + (c - a) = c - b
              @[simp]
              theorem div_mul_div_cancel'' {G : Type u_3} [CommGroup G] (a : G) (b : G) (c : G) :
              a / b * (c / a) = c / b
              @[simp]
              theorem add_sub_sub_cancel {G : Type u_3} [AddCommGroup G] (a : G) (b : G) (c : G) :
              a + b - (a - c) = b + c
              @[simp]
              theorem mul_div_div_cancel {G : Type u_3} [CommGroup G] (a : G) (b : G) (c : G) :
              a * b / (a / c) = b * c
              @[simp]
              theorem sub_sub_sub_cancel_left {G : Type u_3} [AddCommGroup G] (a : G) (b : G) (c : G) :
              c - a - (c - b) = b - a
              @[simp]
              theorem div_div_div_cancel_left {G : Type u_3} [CommGroup G] (a : G) (b : G) (c : G) :
              c / a / (c / b) = b / a
              theorem sub_eq_sub_iff_add_eq_add {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} {d : G} :
              a - b = c - d a + d = c + b
              theorem div_eq_div_iff_mul_eq_mul {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} {d : G} :
              a / b = c / d a * d = c * b
              theorem sub_eq_sub_iff_sub_eq_sub {G : Type u_3} [AddCommGroup G] {a : G} {b : G} {c : G} {d : G} :
              a - b = c - d a - c = b - d
              theorem div_eq_div_iff_div_eq_div {G : Type u_3} [CommGroup G] {a : G} {b : G} {c : G} {d : G} :
              a / b = c / d a / c = b / d
              theorem additive_of_symmetric_of_isTotal {α : Type u_1} {β : Type u_2} [AddMonoid β] (p : ααProp) (r : ααProp) [IsTotal α r] (f : ααβ) (hsymm : Symmetric p) (hf_swap : ∀ {a b : α}, p a bf a b + f b a = 0) (hmul : ∀ {a b c : α}, r a br b cp a bp b cp a cf a c = f a b + f b c) {a : α} {b : α} {c : α} (pab : p a b) (pbc : p b c) (pac : p a c) :
              f a c = f a b + f b c
              theorem multiplicative_of_symmetric_of_isTotal {α : Type u_1} {β : Type u_2} [Monoid β] (p : ααProp) (r : ααProp) [IsTotal α r] (f : ααβ) (hsymm : Symmetric p) (hf_swap : ∀ {a b : α}, p a bf a b * f b a = 1) (hmul : ∀ {a b c : α}, r a br b cp a bp b cp a cf a c = f a b * f b c) {a : α} {b : α} {c : α} (pab : p a b) (pbc : p b c) (pac : p a c) :
              f a c = f a b * f b c
              theorem additive_of_isTotal {α : Type u_1} {β : Type u_2} [AddMonoid β] (r : ααProp) [IsTotal α r] (f : ααβ) (p : αProp) (hswap : ∀ {a b : α}, p ap bf a b + f b a = 0) (hmul : ∀ {a b c : α}, r a br b cp ap bp cf a c = f a b + f b c) {a : α} {b : α} {c : α} (pa : p a) (pb : p b) (pc : p c) :
              f a c = f a b + f b c

              If a binary function from a type equipped with a total relation r to an additive monoid is anti-symmetric (i.e. satisfies f a b + f b a = 0), in order to show it is additive (i.e. satisfies f a c = f a b + f b c), we may assume r a b and r b c are satisfied. We allow restricting to a subset specified by a predicate p.

              theorem multiplicative_of_isTotal {α : Type u_1} {β : Type u_2} [Monoid β] (r : ααProp) [IsTotal α r] (f : ααβ) (p : αProp) (hswap : ∀ {a b : α}, p ap bf a b * f b a = 1) (hmul : ∀ {a b c : α}, r a br b cp ap bp cf a c = f a b * f b c) {a : α} {b : α} {c : α} (pa : p a) (pb : p b) (pc : p c) :
              f a c = f a b * f b c

              If a binary function from a type equipped with a total relation r to a monoid is anti-symmetric (i.e. satisfies f a b * f b a = 1), in order to show it is multiplicative (i.e. satisfies f a c = f a b * f b c), we may assume r a b and r b c are satisfied. We allow restricting to a subset specified by a predicate p.

              @[deprecated div_mul_cancel]
              theorem div_mul_cancel' {G : Type u_3} [Group G] (a : G) (b : G) :
              a / b * b = a

              Alias of div_mul_cancel.

              @[deprecated mul_div_cancel_right]
              theorem mul_div_cancel'' {G : Type u_3} [Group G] (a : G) (b : G) :
              a * b / b = a

              Alias of mul_div_cancel_right.

              @[deprecated div_mul_cancel_right]
              theorem div_mul_cancel''' {G : Type u_3} [Group G] (a : G) (b : G) :
              a / (b * a) = b⁻¹

              Alias of div_mul_cancel_right.

              @[deprecated sub_add_cancel_right]
              theorem sub_add_cancel'' {G : Type u_3} [AddGroup G] (a : G) (b : G) :
              a - (b + a) = -b

              Alias of sub_add_cancel_right.

              @[deprecated mul_div_cancel_left]
              theorem mul_div_cancel''' {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a * b / a = b

              Alias of mul_div_cancel_left.

              @[deprecated add_sub_cancel_left]
              theorem add_sub_cancel' {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a + b - a = b

              Alias of add_sub_cancel_left.

              @[deprecated mul_div_cancel]
              theorem mul_div_cancel'_right {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a * (b / a) = b

              Alias of mul_div_cancel.

              @[deprecated add_sub_cancel]
              theorem add_sub_cancel'_right {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a + (b - a) = b

              Alias of add_sub_cancel.

              @[deprecated div_mul_cancel_left]
              theorem div_mul_cancel'' {G : Type u_3} [CommGroup G] (a : G) (b : G) :
              a / (a * b) = b⁻¹

              Alias of div_mul_cancel_left.

              @[deprecated sub_add_cancel_left]
              theorem sub_add_cancel' {G : Type u_3} [AddCommGroup G] (a : G) (b : G) :
              a - (a + b) = -b

              Alias of sub_add_cancel_left.