leftInvEquiv_symm_mul — Mathlib

English

For x ∈ S, the symmetric equivalence inverse applied to x, multiplied by x, equals 1: ((S.leftInvEquiv hS).symm x : M) * x = 1.

Русский

Для x ∈ S, умножение на x и симметричной обратной через левую эквивалентность даёт единицу.

LaTeX

$$$ ((S.leftInvEquiv hS).symm x : M) * x = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem leftInvEquiv_symm_mul (x : S) : ((S.leftInvEquiv hS).symm x : M) * x = 1 :=
  by
  convert S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)
  simp

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