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 comp_add_left {α : Type u_1} [AddSemigroup α] (x : α) (y : α) : ((fun x => x + x) ∘ fun x => y + x) = fun x => x + y + x

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 => x * x) ∘ fun x => y * x) = fun x => x * y * x

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 => x + x) ∘ fun x => x + y) = fun x => x + (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 => x * x) ∘ fun x => x * y) = fun x => x * (y * x)

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

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 x_1 => x + x_1) 0 = id

theorem one_mul_eq_id {M : Type u} [MulOneClass M] : (fun x x_1 => x * x_1) 1 = id

theorem add_zero_eq_id {M : Type u} [AddZeroClass M] : (fun x => x + 0) = id

theorem mul_one_eq_id {M : Type u} [MulOneClass M] : (fun x => 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 bit0_add {M : Type u} [AddCommSemigroup M] (a : M) (b : M) : bit0 (a + b) = bit0 a + bit0 b

theorem bit1_add {M : Type u} [AddCommSemigroup M] [One M] (a : M) (b : M) : bit1 (a + b) = bit0 a + bit1 b

theorem bit1_add' {M : Type u} [AddCommSemigroup M] [One M] (a : M) (b : M) : bit1 (a + b) = bit1 a + bit0 b

@[simp]

theorem bit0_zero {M : Type u} [AddMonoid M] : bit0 0 = 0

@[simp]

theorem bit1_zero {M : Type u} [AddMonoid M] [One M] : bit1 0 = 1

theorem neg_unique {M : Type u} [AddCommMonoid M] {x : M} {y : M} {z : M} (hy : x + y = 0) (hz : x + z = 0) : y = z

theorem inv_unique {M : Type u} [CommMonoid M] {x : M} {y : M} {z : M} (hy : x * y = 1) (hz : x * z = 1) : y = z

@[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

@[simp]

theorem neg_involutive {G : Type u_3} [InvolutiveNeg G] : Function.Involutive Neg.neg

@[simp]

theorem inv_involutive {G : Type u_3} [InvolutiveInv G] : Function.Involutive Inv.inv

@[simp]

theorem neg_surjective {G : Type u_3} [InvolutiveNeg G] : Function.Surjective Neg.neg

@[simp]

theorem inv_surjective {G : Type u_3} [InvolutiveInv G] : Function.Surjective Inv.inv

theorem neg_injective {G : Type u_3} [InvolutiveNeg G] : Function.Injective Neg.neg

theorem inv_injective {G : Type u_3} [InvolutiveInv G] : Function.Injective Inv.inv

@[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 => -a) fun a => -a

theorem leftInverse_inv (G : Type u_3) [InvolutiveInv G] : Function.LeftInverse (fun a => a⁻¹) fun a => a⁻¹

theorem rightInverse_neg (G : Type u_3) [InvolutiveNeg G] : Function.LeftInverse (fun a => -a) fun a => -a

theorem rightInverse_inv (G : Type u_3) [InvolutiveInv G] : Function.LeftInverse (fun a => a⁻¹) fun a => 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 sub_ne_zero_of_ne {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} : a ≠ b → a - b ≠ 0

theorem div_ne_one_of_ne {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} : a ≠ b → a / 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 SubtractionMonoid.toSubNegZeroMonoid.proof_1 {α : Type u_1} [SubtractionMonoid α] : -0 = 0

instance SubtractionMonoid.toSubNegZeroMonoid {α : Type u_1} [SubtractionMonoid α] : SubNegZeroMonoid α

Equations

• SubtractionMonoid.toSubNegZeroMonoid = let src := SubtractionMonoid.toSubNegMonoid; SubNegZeroMonoid.mk (_ : -0 = 0)

instance DivisionMonoid.toDivInvOneMonoid {α : Type u_1} [DivisionMonoid α] : DivInvOneMonoid α

Equations

• DivisionMonoid.toDivInvOneMonoid = let src := DivisionMonoid.toDivInvMonoid; DivInvOneMonoid.mk (_ : 1⁻¹ = 1)

@[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 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 bit0_neg {α : Type u_1} [SubtractionMonoid α] (a : α) : bit0 (-a) = -bit0 a

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 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)

@[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 x_1 => x + x_1) a)

theorem mul_left_surjective {G : Type u_3} [Group G] (a : G) : Function.Surjective ((fun x x_1 => x * x_1) a)

theorem add_right_surjective {G : Type u_3} [AddGroup G] (a : G) : Function.Surjective fun x => x + a

theorem mul_right_surjective {G : Type u_3} [Group G] (a : G) : Function.Surjective fun x => 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

theorem sub_left_injective {G : Type u_3} [AddGroup G] {b : G} : Function.Injective fun a => a - b

theorem div_left_injective {G : Type u_3} [Group G] {b : G} : Function.Injective fun a => a / b

theorem sub_right_injective {G : Type u_3} [AddGroup G] {b : G} : Function.Injective fun a => b - a

theorem div_right_injective {G : Type u_3} [Group G] {b : G} : Function.Injective fun a => 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 {G : Type u_3} [AddGroup G] (a : G) (b : G) : a + b - b = a

@[simp]

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

@[simp]

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

@[simp]

theorem div_mul_cancel''' {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 = b → a / 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 = b → a - 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 => x - c) fun x => x + c

theorem leftInverse_div_mul_left {G : Type u_3} [Group G] (c : G) : Function.LeftInverse (fun x => x / c) fun x => x * c

theorem leftInverse_add_left_sub {G : Type u_3} [AddGroup G] (c : G) : Function.LeftInverse (fun x => x + c) fun x => x - c

theorem leftInverse_mul_left_div {G : Type u_3} [Group G] (c : G) : Function.LeftInverse (fun x => x * c) fun x => x / c

theorem leftInverse_add_right_neg_add {G : Type u_3} [AddGroup G] (c : G) : Function.LeftInverse (fun x => c + x) fun x => -c + x

theorem leftInverse_mul_right_inv_mul {G : Type u_3} [Group G] (c : G) : Function.LeftInverse (fun x => c * x) fun x => c⁻¹ * x

theorem leftInverse_neg_add_add_right {G : Type u_3} [AddGroup G] (c : G) : Function.LeftInverse (fun x => -c + x) fun x => c + x

theorem leftInverse_inv_mul_mul_right {G : Type u_3} [Group G] (c : G) : Function.LeftInverse (fun x => c⁻¹ * x) fun x => c * x

theorem exists_nsmul_eq_zero_of_zsmul_eq_zero {G : Type u_3} [AddGroup G] {n : ℤ} (hn : n ≠ 0) {x : G} (h : n • x = 0) : ∃ n, 0 < n ∧ n • x = 0

theorem exists_npow_eq_one_of_zpow_eq_one {G : Type u_3} [Group G] {n : ℤ} (hn : n ≠ 0) {x : G} (h : x ^ n = 1) : ∃ n, 0 < n ∧ x ^ n = 1

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' {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 add_sub_cancel'_right {G : Type u_3} [AddCommGroup G] (a : G) (b : G) : a + (b - a) = b

@[simp]

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

@[simp]

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

@[simp]

theorem div_mul_cancel'' {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 b → f a b + f b a = 0) (hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f 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 b → f a b * f b a = 1) (hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f 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 a → p b → f a b + f b a = 0) (hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f 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 a → p b → f a b * f b a = 1) (hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f 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.