zero_divOf

Mathlib.Algebra.MonoidAlgebra.Division

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.zero_divOf

English

Dividing the zero element by any g yields zero.

Русский

Деление нуля на любое g дает нуль.

LaTeX

$$$$0/divOf g = 0.$$$$

Lean4

@[simp]
theorem zero_divOf (g : G) : (0 : k[G]) /ᵒᶠ g = 0 :=
  map_zero (Finsupp.comapDomain.addMonoidHom _)

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

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

Разделы

Аффилиация

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