mul_leftInvEquiv — Mathlib

English

For x ∈ S.leftInv, the product x * (S.leftInvEquiv hS x) equals the identity: x * (S.leftInvEquiv hS x) = 1.

Русский

Для x ∈ S.leftInv произведение x на образ через эквивалентность равно единице: x * (S.leftInvEquiv hS x) = 1.

LaTeX

$$$ x * (S.leftInvEquiv hS x) = 1 $$$

Lean4

@[to_additive]
theorem mul_leftInvEquiv (x : S.leftInv) : (x : M) * S.leftInvEquiv hS x = 1 := by
  simp only [leftInvEquiv_apply, fromCommLeftInv, mul_fromLeftInv]

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