stabilizerEquivStabilizer_one — Mathlib

English

The stabilizerEquivStabilizer for the identity action is the identity on stabilizers.

Русский

StabilizerEquivStabilizer для единичного действия совпадает с тождественным изоморфизмом стабилизаторов.

LaTeX

$$stabilizerEquivStabilizer (one_smul G a).symm = MulEquiv.refl (stabilizer G a)$$

Lean4

theorem stabilizerEquivStabilizer_one :
    stabilizerEquivStabilizer (one_smul G a).symm = MulEquiv.refl (stabilizer G a) := by ext;
  simp [stabilizerEquivStabilizer_apply]

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