toNonUnitalNonAssocSemiring_injective

English

The forgetful map from NonAssocSemiring to NonUnitalNonAssocSemiring is injective: if two NonAssocSemiring structures become equal after forgetting the multiplication, then the original structures are equal.

Русский

Отображение забывания структуры NonAssocSemiring на NonUnitalNonAssocSemiring инъективно: если две структуры NonAssocSemiring совпадают после забывания умножения, то сами структуры равны.

LaTeX

$$$\\\\forall A,B \\,\\in \\, \\text{NonAssocSemiring}(R), \\\\text{toNonUnitalNonAssocSemiring}(A) = \\\\text{toNonUnitalNonAssocSemiring}(B) \\\\Rightarrow A = B.$$$

Lean4

theorem toNonUnitalNonAssocSemiring_injective : Function.Injective (@toNonUnitalNonAssocSemiring R) :=
  by
  intro _ _ _
  ext <;> congr

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