fromLeftInv_eq_iff — Mathlib

English

Let a ∈ S.leftInv and b ∈ M. Then (S.fromLeftInv a : M) = b if and only if (a : M) * b = 1. This characterizes when b is the right inverse of a within M.

Русский

Пусть a ∈ S.leftInv и b ∈ M. Тогда (S.fromLeftInv a : M) = b тогда и только тогда, когда (a : M) * b = 1. Это характеристика того, когда b является правым обратным к a в M.

LaTeX

$$$ (S.fromLeftInv\ a : M) = b \\iff (a : M) * b = 1 $$$

Lean4

@[to_additive]
theorem fromLeftInv_eq_iff (a : S.leftInv) (b : M) : (S.fromLeftInv a : M) = b ↔ (a : M) * b = 1 := by
  rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]

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