of'_modOf

Mathlib.Algebra.MonoidAlgebra.Division

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.of'_modOf

English

The remainder of the basis element by itself is zero.

Русский

Остаток базисного элемента от себя равен нулю.

LaTeX

$$$ \\operatorname{modOf}(\\operatorname{of}'(g), g) = 0 $$$

Lean4

theorem of'_modOf (g : G) : of' k G g %ᵒᶠ g = 0 := by simpa only [one_mul] using mul_of'_modOf (1 : k[G]) g

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru