inv_zero

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.inv_zero

English

Inverse of zero is zero.

Русский

Обратный нулю равен нулю.

LaTeX

$$$ (0)^{-1} = 0 $$$

Lean4

@[simp]
protected theorem inv_zero : (0 : tsze R M)⁻¹ = (0 : tsze R M) := by rw [← inl_zero, TrivSqZeroExt.inv_inl, inv_zero]

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

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

Разделы

Аффилиация

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