divOfHom — Mathlib

English

Multiplying by the element of a monomial then dividing by that same element yields the original polynomial.

Русский

Умножение на элемент и деление тем же элементом возвращает исходный полином.

LaTeX

$$$$ x \cdot of'\ k G a /ᵒᶠ a = x. $$$$

Lean4

/-- A bundled version of `AddMonoidAlgebra.divOf`. -/
@[simps]
noncomputable def divOfHom : Multiplicative G →* AddMonoid.End k[G]
    where
  toFun
    g :=
    { toFun := fun x => divOf x g.toAdd
      map_zero' := zero_divOf _
      map_add' := fun x y => add_divOf x y g.toAdd }
  map_one' := AddMonoidHom.ext divOf_zero
  map_mul' g₁ g₂ := AddMonoidHom.ext fun _x => (congr_arg _ (add_comm g₁.toAdd g₂.toAdd)).trans (divOf_add _ _ _)

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