monoidHomCongrLeftEquiv_refl — Mathlib

English

The left-congruence induced by the identity on M is the identity on the function space M →* N.

Русский

Левая эквивалентность, порожденная тождественным отображением на M, является тождественной на пространстве MonoidHom M →* N.

LaTeX

$$$\operatorname{monoidHomCongrLeftEquiv}(\mathrm{refl}\, M) = \mathrm{refl}\ (M \to^* N)$. $$

Lean4

@[to_additive (attr := simp)]
theorem monoidHomCongrLeftEquiv_refl : monoidHomCongrLeftEquiv (.refl M) = .refl (M →* N) :=
  rfl

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