mk_leftInverse — Mathlib

English

The map mk g is left-inverse to modByMonicHom hg, i.e., composing mk g with modByMonicHom hg yields the identity on AdjoinRoot g.

Русский

Изображение mk g является левым обратным к modByMonicHom hg, т.е. композиция mk g ∘ modByMonicHom hg — тождественное на AdjoinRoot g.

LaTeX

$$LeftInverse mk g and modByMonicHom hg$$

Lean4

theorem mk_leftInverse (hg : g.Monic) : Function.LeftInverse (mk g) (modByMonicHom hg) :=
  by
  intro f
  induction f using AdjoinRoot.induction_on
  rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel_left, dvd_neg]
  apply dvd_mul_right

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