The embedding of a cancellative semigroup into itself by multiplication by a fixed element. #
def
addLeftEmbedding.proof_1
{G : Type u_1}
[inst : AddLeftCancelSemigroup G]
(g : G)
:
Function.Injective ((fun x x_1 => x + x_1) g)
Equations
- (_ : Function.Injective ((fun x x_1 => x + x_1) g)) = (_ : Function.Injective ((fun x x_1 => x + x_1) g))
The embedding of a left cancellative additive semigroup into itself by left translation by a fixed element.
Equations
- addLeftEmbedding g = { toFun := fun h => g + h, inj' := (_ : Function.Injective ((fun x x_1 => x + x_1) g)) }
@[simp]
theorem
mulLeftEmbedding_apply
{G : Type u_1}
[inst : LeftCancelSemigroup G]
(g : G)
(h : G)
:
↑(mulLeftEmbedding g) h = g * h
@[simp]
theorem
addLeftEmbedding_apply
{G : Type u_1}
[inst : AddLeftCancelSemigroup G]
(g : G)
(h : G)
:
↑(addLeftEmbedding g) h = g + h
The embedding of a left cancellative semigroup into itself by left multiplication by a fixed element.
Equations
- mulLeftEmbedding g = { toFun := fun h => g * h, inj' := (_ : Function.Injective ((fun x x_1 => x * x_1) g)) }
def
addRightEmbedding.proof_1
{G : Type u_1}
[inst : AddRightCancelSemigroup G]
(g : G)
:
Function.Injective fun x => x + g
Equations
- (_ : Function.Injective fun x => x + g) = (_ : Function.Injective fun x => x + g)
The embedding of a right cancellative additive semigroup into itself by right translation by a fixed element.
Equations
- addRightEmbedding g = { toFun := fun h => h + g, inj' := (_ : Function.Injective fun x => x + g) }
@[simp]
theorem
addRightEmbedding_apply
{G : Type u_1}
[inst : AddRightCancelSemigroup G]
(g : G)
(h : G)
:
↑(addRightEmbedding g) h = h + g
@[simp]
theorem
mulRightEmbedding_apply
{G : Type u_1}
[inst : RightCancelSemigroup G]
(g : G)
(h : G)
:
↑(mulRightEmbedding g) h = h * g
The embedding of a right cancellative semigroup into itself by right multiplication by a fixed element.
Equations
- mulRightEmbedding g = { toFun := fun h => h * g, inj' := (_ : Function.Injective fun x => x * g) }
theorem
add_left_embedding_eq_add_right_embedding
{G : Type u_1}
[inst : AddCancelCommMonoid G]
(g : G)
:
theorem
mul_left_embedding_eq_mul_right_embedding
{G : Type u_1}
[inst : CancelCommMonoid G]
(g : G)
: