inv_inr — Mathlib

English

In a trivial square-zero extension, every element coming from M has multiplicative inverse equal to 0.

Русский

Во тривиальном расширении с нулевой квадратичностью элемент, полученный из M, имеет обратный равный нулю.

LaTeX

$$$ (inr\\, m)^{-1} = 0 $$$

Lean4

@[simp]
theorem inv_inr (m : M) : (inr m)⁻¹ = (0 : tsze R M) := by
  ext
  · rw [fst_inv, fst_inr, fst_zero, inv_zero]
  · rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_zero]

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