normalizedFactorsEquiv_symm_apply

English

Definition of a bijection between two factor multisets given a commuting with normalization and a MulEquiv.

Русский

Определение биекции между двумя мультимирес фактов заданное коммутированием нормализации и MulEquiv.

LaTeX

$$def normalizedFactorsEquiv (...) := Equiv.subtypeEquiv f (..) $$

Lean4

@[simp]
theorem normalizedFactorsEquiv_symm_apply (he : ∀ x, normalize (f x) = f (normalize x)) {a : α} {q : β}
    (hq : q ∈ normalizedFactors (f a)) :
    (normalizedFactorsEquiv he a).symm ⟨q, hq⟩ = (MulEquivClass.toMulEquiv f).symm q :=
  rfl

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