mul_left_eq_one — Mathlib

English

If r ∈ R and x ∈ tsze_R M satisfy r * fst(x) = 1, then multiplying a certain combination with x yields 1 on the left; this provides a left-inverse identity.

Русский

Если r ∈ R и fst(x) удовлетворяет r⋅fst(x)=1, то определённая комбинация даёт левую единицу при умножении на x.

LaTeX

$$$ r \\cdot fst(x) = 1 \\Rightarrow (inl r + inr( -((r \\gt x.snd) \\<• r) )) \\cdot x = 1$$$

Lean4

theorem mul_left_eq_one (r : R) (x : tsze R M) (h : r * x.fst = 1) : (inl r + inr (-((r •> x.snd) <• r))) * x = 1 :=
  by
  ext <;> dsimp
  · rw [add_zero, h]
  · rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul, add_neg_cancel]

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