Composing two associative operations of f : α → α → α
on the left
is equal to an associative operation on the left.
Composing two associative operations of f : α → α → α
on the right
is equal to an associative operation on the right.
@[simp]
theorem
comp_add_left
{α : Type u_1}
[add_semigroup α]
(x y : α) :
has_add.add x ∘ has_add.add y = has_add.add (x + y)
Composing two additions on the left by y
then x
is equal to a addition on the left by x + y
.
@[simp]
theorem
comp_mul_left
{α : Type u_1}
[semigroup α]
(x y : α) :
has_mul.mul x ∘ has_mul.mul y = has_mul.mul (x * y)
Composing two multiplications on the left by y
then x
is equal to a multiplication on the left by x * y
.
@[simp]
Composing two additions on the right by y
and x
is equal to a addition on the right by y + x
.
theorem
inv_unique
{M : Type u}
[comm_monoid M]
{x y z : M}
(hy : x * y = 1)
(hz : x * z = 1) :
y = z
theorem
neg_unique
{M : Type u}
[add_comm_monoid M]
{x y z : M}
(hy : x + y = 0)
(hz : x + z = 0) :
y = z
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
left_inverse_neg
(G : Type u_1)
[add_group G] :
function.left_inverse (λ (a : G), -a) (λ (a : G), -a)
theorem
left_inverse_inv
(G : Type u_1)
[group G] :
function.left_inverse (λ (a : G), a⁻¹) (λ (a : G), a⁻¹)
theorem
add_right_surjective
{G : Type u}
[add_group G]
(a : G) :
function.surjective (λ (x : G), x + a)
theorem
mul_right_surjective
{G : Type u}
[group G]
(a : G) :
function.surjective (λ (x : G), x * a)
theorem
sub_left_injective
{G : Type u}
[add_group G]
{b : G} :
function.injective (λ (a : G), a - b)
theorem
sub_right_injective
{G : Type u}
[add_group G]
{b : G} :
function.injective (λ (a : G), b - a)
theorem
left_inverse_sub_add_left
{G : Type u}
[add_group G]
(c : G) :
function.left_inverse (λ (x : G), x - c) (λ (x : G), x + c)
theorem
left_inverse_add_left_sub
{G : Type u}
[add_group G]
(c : G) :
function.left_inverse (λ (x : G), x + c) (λ (x : G), x - c)
theorem
left_inverse_add_right_neg_add
{G : Type u}
[add_group G]
(c : G) :
function.left_inverse (λ (x : G), c + x) (λ (x : G), -c + x)
theorem
left_inverse_neg_add_add_right
{G : Type u}
[add_group G]
(c : G) :
function.left_inverse (λ (x : G), -c + x) (λ (x : G), c + x)
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]