inv_mul_cancel_left

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#Units.inv_mul_cancel_left

English

For a ∈ α^× and b ∈ α, a^{-1} · (a · b) = b.

Русский

Для a ∈ α^× и b ∈ α выполняется a^{-1} · (a · b) = b.

LaTeX

$$$ a^{-1} \cdot (a \cdot b) = b$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_mul_cancel_left (a : αˣ) (b : α) : (↑a⁻¹ : α) * (a * b) = b := by rw [← mul_assoc, inv_mul, one_mul]

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

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

Разделы

Аффилиация

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