mul

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#IsUnit.mul

English

If a and b are units, then their product is a unit.

Русский

Если a и b — единицы, то их произведение — единица.

LaTeX

$$IsUnit(a) \rightarrow IsUnit(b) \rightarrow IsUnit(a \cdot b)$$

Lean4

@[to_additive]
theorem mul : IsUnit a → IsUnit b → IsUnit (a * b) := by rintro ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨x * y, rfl⟩

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

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

Разделы

Аффилиация

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