ofFixingSubgroup_of_eq_bijective — Mathlib

English

If s = t, the corresponding fixing-subgroup equivalence is bijective.

Русский

При s = t соответствующее эквивалентное преобразование фиксационной подгруппы биективно.

LaTeX

$$$\text{Bijective}(\mathrm{ofFixingSubgroup\_of\_eq}\ M hst)$$$

Lean4

@[to_additive]
theorem ofFixingSubgroup_of_eq_bijective {hst : s = t} : Bijective (ofFixingSubgroup_of_eq M hst) :=
  ⟨fun _ _ hxy ↦ by simpa [← SetLike.coe_eq_coe] using hxy, fun ⟨x, hxt⟩ ↦
    ⟨⟨x, by rwa [hst]⟩, by simp [← SetLike.coe_eq_coe]⟩⟩

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