ofFixingSubgroup_of_eq_apply — Mathlib

English

The application formula for the equality case of fixing subgroups is the identity on the underlying set.

Русский

Применение для случая равенства фиксационных подгрупп даёт тождественный переход на множество.

LaTeX

$$$\text{eq\_apply: }(\mathrm{ofFixingSubgroup\_of\_eq\_apply}\ M hst x) = x$$$

Lean4

@[to_additive (attr := simp)]
theorem ofFixingSubgroup_of_eq_apply {hst : s = t} (x : ofFixingSubgroup M s) :
    ((ofFixingSubgroup_of_eq M hst x) : α) = x :=
  rfl

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