of'_mul_divOf — Mathlib

English

Multiplying by a monomial on the left and then dividing by that same exponent recovers the original x.

Русский

Умножение слева мономом и деление тем же основанием восстанавливает x.

LaTeX

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

Lean4

theorem of'_mul_divOf (a : G) (x : k[G]) : of' k G a * x /ᵒᶠ a = x :=
  by
  ext
  rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
  intro c hc
  exact add_right_inj _

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