subgroupCongr_apply — Mathlib

English

The subgroupCongr construction acts as the identity on elements when the two subgroups are equal: (subgroupCongr h x : G) = x.

Русский

Конструкция subgroupCongr действует как тождество на элементах при равенстве подгрупп: (subgroupCongr h x : G) = x.

LaTeX

$$$\\text{If } h: H=K,\\; (\\operatorname{subgroupCongr}\\, h\\, x : G) = x$$$

Lean4

@[to_additive (attr := simp)]
theorem subgroupCongr_apply (h : H = K) (x) : (MulEquiv.subgroupCongr h x : G) = x :=
  rfl

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