map_inl — Mathlib

English

An instance of MulEquivClass for Equiv between group extensions exists, linking E and E'.

Русский

Существует экземпляр MulEquivClass для эквивалентностей между группами-расширениями, связывающий E и E'.

LaTeX

$$$\\operatorname{MulEquivClass}(S.\\Equiv S')\\; E\\; E'$$$

Lean4

@[to_additive (attr := simp)]
theorem map_inl (n : N) : equiv (S.inl n) = S'.inl n :=
  congrFun equiv.inl_comm n

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