mul_leftInvEquiv_symm — Mathlib

English

For x ∈ S, the product of x with the symmetric inverse under leftInvEquiv equals 1: (x : M) * (S.leftInvEquiv hS).symm x = 1.

Русский

Для x ∈ S произведение x на симметричный обратный через leftInvEquiv даёт 1.

LaTeX

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

Lean4

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

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