mker_inr — Mathlib

English

Let M and N be multiplicative monoids. The kernel of the right-inclusion map inr from M to M × N is the trivial submonoid, i.e. only the identity of M maps to the identity of the product.

Русский

Пусть M и N — моноиды. Ядро правого включения inr из M в M × N равно тривиальному подмонойду: единственный элемент M, отображающийся в единицу пары (1_M, 1_N).

LaTeX

$$$ \operatorname{mker}(\operatorname{inr} M N) = \bot $$$

Lean4

@[to_additive (attr := simp)]
theorem mker_inr : mker (inr M N) = ⊥ := by
  ext x
  simp [mem_mker]

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