selfEquivSigmaOrbitsQuotientStabilizer

English

A specialization of the class formula for φ = Quotient.out giving a bijection β ≃ Σ ω : Ω, α / Stab(φ ω).

Русский

Специализация классической формулы для φ = Quotient.out даёт биекцию β ≃ Σ ω : Ω, α / Stab(φ(ω)).

LaTeX

$$$\beta \cong \Sigma_{\omega \in \Omega} \alpha \/\!\!\!\-\!\!\! / \operatorname{stabilizer}(\alpha, \omega^{\mathrm{out}}).$$$

Lean4

/-- **Class formula**. This is a special case of
`MulAction.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = Quotient.out`. -/
@[to_additive /-- **Class formula**. This is a special case of
          `AddAction.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = Quotient.out`. -/
    ]
noncomputable def selfEquivSigmaOrbitsQuotientStabilizer : β ≃ Σ ω : Ω, α ⧸ stabilizer α ω.out :=
  selfEquivSigmaOrbitsQuotientStabilizer' α β Quotient.out_eq'

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