withOneCongr_refl — Mathlib

English

The with-one congruence of the reflexive equal is equal to the reflexive in WithOne: (MulEquiv.refl α).withOneCongr = MulEquiv.refl (WithOne α).

Русский

Соответствие с единицей сохраняется в пределах WithOne для тождества: (MulEquiv.refl α).withOneCongr = MulEquiv.refl (WithOne α).

LaTeX

$$$(\mathrm{MulEquiv.refl}\ \alpha).\mathrm{withOneCongr} = \mathrm{MulEquiv.refl}\ (\mathrm{WithOne}\ \alpha)$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.MulEquiv.withOneCongr_refl : (MulEquiv.refl α).withOneCongr = MulEquiv.refl _ :=
  MulEquiv.toMonoidHom_injective mapMulHom_id

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