mulLeft₀_symm

Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso

URI: https://scilib.ai/kg/mathlib#OrderIso.mulLeft₀_symm

English

Symmetry of the left multiplication order isomorphism: (mulLeft₀ a)^{-1} equals mulLeft₀ a^{-1}.

Русский

Симметрична лево-умножающая изоморфия: (mulLeft₀ a)^{-1} = mulLeft₀ a^{-1}.

LaTeX

$$(mulLeft₀ a)^{-1} = mulLeft₀ a^{-1}$$

Lean4

theorem mulLeft₀_symm (a : G₀) (ha : 0 < a) : (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ (inv_pos.2 ha) := by ext; rfl

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

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

Разделы

Аффилиация

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