liftOfRightInverseAux_comp_apply — Mathlib

English

The auxiliary lift φ = liftOfRightInverseAux satisfies φ(f(a)) = g(a) for all a in A.

Русский

Вспомогательный лифт φ = liftOfRightInverseAux удовлетворяет φ(f(a)) = g(a) для всех a ∈ A.

LaTeX

$$$$ (f.liftOfRightInverseAux f_{inv} hf g hg)(f(a)) = g(a). $$$$

Lean4

@[simp]
theorem liftOfRightInverseAux_comp_apply (hf : Function.RightInverse f_inv f) (g : A →+* C)
    (hg : RingHom.ker f ≤ RingHom.ker g) (a : A) : (f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a :=
  f.toAddMonoidHom.liftOfRightInverse_comp_apply f_inv hf ⟨g.toAddMonoidHom, hg⟩ a

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