mulLeftEmbedding_eq_mulRightEmbedding

English

For any CommMagma G with IsCancelMul, the left and right embeddings by g coincide: mulLeftEmbedding g = mulRightEmbedding g for all g ∈ G.

Русский

Для любого CommMagma G с IsCancelMul левые и правые вложения умножения на g совпадают: mulLeftEmbedding g = mulRightEmbedding g для всех g ∈ G.

LaTeX

$$$\\\\forall G \\\\[CommMagma G] \\\\forall g \\\\in G, \\\\text{mulLeftEmbedding}(g) = \\\\text{mulRightEmbedding}(g)$$$

Lean4

@[to_additive]
theorem mulLeftEmbedding_eq_mulRightEmbedding [CommMagma G] [IsCancelMul G] (g : G) :
    mulLeftEmbedding g = mulRightEmbedding g := by
  ext
  exact mul_comm _ _

Похожие утверждения