of'_divOf — Mathlib

English

In the monoid algebra over a semiring k, the quotient of the basis element corresponding to a by a is the multiplicative identity.

Русский

В моноидной алгебре над полем k деление базисного элемента, соответствующего элементу a из группы G на a дает единицу умножения.

LaTeX

$$$ \\bigl( \\operatorname{of}' k G a \\bigr) /^{\\circ a} = 1$$$

Lean4

theorem of'_divOf (a : G) : of' k G a /ᵒᶠ a = 1 := by simpa only [one_mul] using mul_of'_divOf (1 : k[G]) a

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