stabilizerEquivStabilizer_symm — Mathlib

English

The symmetric of stabilizer equivalence equals the stabilizer equivalence for the negated relation.

Русский

Симметрическая стабилизаторная эквивелентность равна эквивелентности для противоположного отношения.

LaTeX

$$$\\bigl( \\mathrm{stabilizerEquivStabilizer } hg \\bigr)^{\\!\\!} = \\mathrm{stabilizerEquivStabilizer} (eq\\_neg\\_vadd\_iff.mpr hg.symm).$$$

Lean4

theorem stabilizerEquivStabilizer_symm (hg : b = g +ᵥ a) :
    (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer (eq_neg_vadd_iff.mpr hg.symm) := by ext;
  simp [stabilizerEquivStabilizer]

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