mul_one

Mathlib.NumberTheory.MulChar.Basic

URI: https://scilib.ai/kg/mathlib#MulChar.mul_one

← MathLib Explorer

English

The identity element on the right leaves a character unchanged: χ · 1 = χ.

Русский

Единица справа не изменяет характер: χ · 1 = χ.

LaTeX

$$$$ \\chi \\cdot 1 = \\chi. $$$$

Lean4

protected theorem mul_one (χ : MulChar R R') : χ * 1 = χ :=
  by
  ext
  simp only [mul_one, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]

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

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

Разделы

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

Аффилиация

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