mul_of'_divOf

Mathlib.Algebra.MonoidAlgebra.Division

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.mul_of'_divOf

← MathLib Explorer

English

A repetition of the left-multiplication/division property by a monomial.

Русский

Повторение свойства левого умножения/деления мономом.

LaTeX

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

Lean4

theorem mul_of'_divOf (x : k[G]) (a : G) : x * of' k G a /ᵒᶠ a = x :=
  by
  ext
  rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]
  intro c hc
  rw [add_comm]
  exact add_right_inj _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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